, En effet, il n'est pas possible en l'état de définir une matrice diagonale par blocs dont les blocs sont eux-mêmes des matrices diagonales par blocs, l'obstacle technique étant le même que celui décrit à la section 4 pour les matrices compagnes Notre prochain objectif est d'utiliser les notions définies ici comme spécification pour une implémentation efficace d'un algorithme de calcul de la forme de Frobenius. Par exemple, celui décrit dans [Sto01] a une complexité en O(n ? log n log log n) pour une implémentation du produit matriciel en O(n ? ) et serait un bon candidat car il est déterministe. Une sous-routine de cet algorithme est connue sous le nom d
, e) trouvera les sources complètes du développement formel présenté dans cet article, ainsi qu'une documentation hypertexte, à l'adresse : http://www-sop. inria
, Siles : Smith Normal form and executable rank for matrices, 2012.
, Formalized algebraic numbers : construction and first order theory, Thèse de doctorat, École Polytechnique, 2012.
, Les neuf chapitres le classique mathématique de la Chine ancienne et ses commentaires, 2004.
, Siles : A refinement-based approach to computational algebra in coq Giesbrecht : Nearly optimal algorithms for canonical matrix forms, Interactive Theorem Proving, pp.83-98948, 1995.
, A Small Scale Reflection Extension for the Coq system, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384
, Fast algorithms for the characteristics polynomial, Theoretical Computer Science, vol.36, pp.309-317, 1985.
DOI : 10.1016/0304-3975(85)90049-0
, Formalisation des mathématiques : une preuve du théorème de Cayley- Hamilton, JFLA (Journées Francophones des Langages Applicatifs), pp.1-14, 2008.