Matrices à blocs et en forme canonique - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Matrices à blocs et en forme canonique

(1) , (1)
1
Guillaume Cano
  • Function : Author
  • PersonId : 935708
Maxime Dénès
  • Function : Author
  • PersonId : 904380

Abstract

Nous présentons une formalisation réalisée avec Coq visant essentiellement à prouver l'existence des formes matricielles canoniques de Frobenius et de Jordan, ainsi que leurs propriétés. Nous définissons formellement des notions importantes, comme les matrices diagonales par blocs ou les matrices compagnes, et prouvons des résultats intermédiaires originaux, comme le théorème fondamental de similitude sur un corps, ou encore l'unicité de la forme normale de Smith. Outre la formalisation de la théorie de la réduction des endormorphismes des espaces vectoriels de dimension finie, ce travail ouvre la voie à la certification d'algorithmes efficaces de calcul du polynôme caractéristique ou de la forme de Frobenius.
Fichier principal
Vignette du fichier
jfla2013-04.pdf (416.3 Ko) Télécharger le fichier
Origin : Explicit agreement for this submission
Loading...

Dates and versions

hal-00779376 , version 1 (22-01-2013)

Identifiers

  • HAL Id : hal-00779376 , version 1

Cite

Guillaume Cano, Maxime Dénès. Matrices à blocs et en forme canonique. JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00779376⟩
280 View
2241 Download

Share

Gmail Facebook Twitter LinkedIn More