Matrices à blocs et en forme canonique

Guillaume Cano 1 Maxime Dénès 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00779376
Contributor : Ist Inria Saclay <>
Submitted on : Tuesday, January 22, 2013 - 10:40:57 AM
Last modification on : Thursday, January 11, 2018 - 4:21:55 PM
Long-term archiving on : Saturday, April 1, 2017 - 8:08:13 AM

File

jfla2013-04.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-00779376, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

369

Files downloads

2489