Mathlib Map

Map · 20

group theory

MSC 20 · Group theory and generalizations

27,204 declarations (21,151 theorems, 6,053 definitions) across 456 files. 9 of the 55 famous theorems listed for this area are in Mathlib (16%). 26 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas12

  • 20M Semigroups 11,795
  • 20D Abstract finite groups 6,684
  • 20E Structure and classification of infinite or finite groups 2,041
  • 20B Permutation groups 1,975
  • 20C Representation theory of groups 1,201
  • 20J Connections of group theory with homological algebra and category theory 904
  • 20K Abelian groups 865
  • 20F Special aspects of infinite or finite groups 826
  • 20G Linear algebraic groups and related topics 572
  • 20N Other generalizations of groups 198
  • 20L Groupoids (i.e. small categories in which all morphisms are isomorphisms) 139
  • 20A Foundations 4

Famous theorems9 of 55

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 46

In Mathlib · 9

From the 100 theorems list3

Open conjectures stated in Lean26

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing7 of 39

From Mathlib's own undergraduate checklist.

Group Theory · 7 of 39

  • Representation theory of finite groups › representations of abelian groups
  • Representation theory of finite groups › dual groups
  • Representation theory of finite groups › Fourier transform for finite abelian groups
  • Representation theory of finite groups › convolution
  • Representation theory of finite groups › class function over a group
  • Representation theory of finite groups › orthonormal basis of irreducible characters
  • Representation theory of finite groups › examples of groups with small cardinality

Structures defined here24

Typeclasses defined in this area's files, most assumed first.

Files456

Largest first. The code after each file is its assigned subarea.