Skip to Main content Skip to Navigation
Conference papers

Finite groups representation theory with Coq

Sidi Ould Biha 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Representation theory is a branch of algebra that allows the study of groups through linear applications, i.e. matrices. Thus problems in abstract groups can be reduced to problems on matrices. Representation theory is the basis of character theory. In this paper we present a formalization of finite groups representation theory in the Coq system that includes a formalization of Maschke's theorem on reducible finite group algebra. This work is a part of the Mathematical Components project which aims to develop a formal proof of the Feit-Thompson theorem.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Sidi Ould Biha Connect in order to contact the contributor
Submitted on : Tuesday, April 21, 2009 - 5:25:27 PM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Friday, October 12, 2012 - 5:10:59 PM


Files produced by the author(s)


  • HAL Id : inria-00377431, version 1



Sidi Ould Biha. Finite groups representation theory with Coq. 8th International Conference on Mathematical Knowledge Management, Jul 2009, Grand Bend, Ontario, Canada. ⟨inria-00377431⟩



Record views


Files downloads