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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00202795
Contributor : Sandrine Blazy <>
Submitted on : Tuesday, January 8, 2008 - 10:55:56 AM
Last modification on : Thursday, January 11, 2018 - 4:22:53 PM
Document(s) archivé(s) le : Thursday, September 27, 2012 - 1:51:01 PM

File

ouldbiha.pdf
Explicit agreement for this submission

Identifiers

  • 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), INRIA, Jan 2008, Etretat, France. pp.1-14. ⟨inria-00202795⟩

Share

Metrics

Record views

349

Files downloads

310