Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton

Sidi Ould Biha 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Le théorème de Cayley-Hamilton est l'un des principaux théorèmes de l'algèbre linéaire. Dans cet article, nous présentons une première formalisation dans un assistant à la preuve de ce théorème. Cette formalisation a été développée dans Coq en utilisant son extension SSReflect développée par G. Gonthier. Ce travail repose sur des développements sur les matrices, les polynômes et les opérations indexées. Il rentre dans le cadre des travaux de formalisation du théorème de Feit-Thompson sur les groupes solvables.
Type de document :
Communication dans un congrès
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.1-14, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00202795
Contributeur : Sandrine Blazy <>
Soumis le : mardi 8 janvier 2008 - 10:55:56
Dernière modification le : jeudi 11 janvier 2018 - 16:22:53
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:51:01

Fichier

ouldbiha.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00202795, version 1

Collections

Citation

Sidi Ould Biha. Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton. JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.1-14, 2008. 〈inria-00202795〉

Partager

Métriques

Consultations de la notice

314

Téléchargements de fichiers

265