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

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.