Point-Free, Set-Free Concrete Linear Algebra - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Point-Free, Set-Free Concrete Linear Algebra

Georges Gonthier
  • Function : Author
  • PersonId : 839098


We show how a simple variant of Gaussian elimination can be used to model abstract linear algebra directly, using matrices only to represent all categories of objects, with operations such as subspace intersection and sum. We can even provide effective support for direct sums and subalgebras. We have formalized this work in Coq, and used it to develop all of the group representation theory required for the proof of the Odd Order Theorem, including results such as the Jacobson Density Theorem, Clifford's Theorem, the Jordan-Holder Theorem for modules, the Wedderburn Structure Theorem for semisimple rings (the basis for character theory).
On présente une formalisation en Coq de l'algèbre linéaire où tous les objets sont représentés par des matrices, y compris les sous-espaces. Ce développement a été utilisé pour élaborer la formalisation des éléments de théorie de la représentation nécessaires à la prévue du théorème de Feit-Thompson.
Fichier principal
Vignette du fichier
main.pdf (170.6 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00805966 , version 1 (29-03-2013)



Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. Interactive Theorem Proving - ITP 2011, Radboud University of Nijmegen, Aug 2011, Berg en Dal, Netherlands. pp.103-118, ⟨10.1007/978-3-642-22863-6_10⟩. ⟨hal-00805966⟩


313 View
689 Download



Gmail Facebook Twitter LinkedIn More