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.
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00779376
Contributeur : Ist Inria Saclay <>
Soumis le : mardi 22 janvier 2013 - 10:40:57
Dernière modification le : jeudi 11 janvier 2018 - 16:21:55
Document(s) archivé(s) le : samedi 1 avril 2017 - 08:08:13

Fichier

jfla2013-04.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00779376, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

337

Téléchargements de fichiers

2137