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.
https://hal.inria.fr/inria-00202795
Contributor : Sandrine Blazy <>
Submitted on : Tuesday, January 8, 2008 - 10:55:56 AM Last modification on : Thursday, January 7, 2021 - 3:40:05 PM Long-term archiving on: : Thursday, September 27, 2012 - 1:51:01 PM
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⟩