Finite Groups Representation Theory with Coq
| Autor: | Sidi Ould Biha |
|---|---|
| Přispěvatelé: | Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Ould Biha, Sidi |
| Rok vydání: | 2009 |
| Předmět: |
Modular representation theory
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory Group (mathematics) 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 01 natural sciences Algebra Faithful representation Representation theory of the symmetric group 010201 computation theory & mathematics ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.4: Mechanical theorem proving Trivial representation 0101 mathematics Maschke's theorem Representation theory of finite groups Group theory Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642026133 Calculemus/MKM 8th International Conference on Mathematical Knowledge Management 8th International Conference on Mathematical Knowledge Management, Jul 2009, Grand Bend, Ontario, Canada |
| DOI: | 10.1007/978-3-642-02614-0_34 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|