Point-Free, Set-Free Concrete Linear Algebra

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

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00805966
Contributor : Georges Gonthier <>
Submitted on : Friday, March 29, 2013 - 3:03:50 PM
Last modification on : Friday, March 29, 2013 - 3:51:27 PM
Document(s) archivé(s) le : Sunday, June 30, 2013 - 4:00:42 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

458

Files downloads

457