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
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
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〉
