Group Theory

Lagrange's Theorem

Subgroup order divides group order

lean4-proofgroup-theoryvisualization

Cayley's Theorem

Every group embeds into a symmetric group

lean4-proofgroup-theoryvisualization

Sylow Theorems

Prime-power subgroups always exist, are conjugate, and their count is constrained

lean4-proofgroup-theoryvisualization

First Isomorphism Theorem

The image of a homomorphism is isomorphic to the domain modulo the kernel

lean4-proofgroup-theoryvisualization

Cauchy's Theorem (Groups)

If a prime p divides |G| then G has an element of order p

lean4-proofgroup-theoryvisualization

Burnside's Lemma

The number of orbits equals the average size of fixed-point sets over the group.

lean4-proofgroup-theoryvisualization

Class Equation

The order of a finite group equals the size of its center plus the sum of sizes of nontrivial conjugacy classes.

lean4-proofgroup-theoryvisualization

FTAG (Finite Abelian)

Every finite abelian group decomposes as a direct sum of cyclic groups of prime power order.

lean4-proofgroup-theoryvisualization

Solvable Group

A group is solvable if its derived series reaches the trivial group in finitely many steps.

lean4-proofgroup-theoryvisualization

Nilpotent Group

A group is nilpotent if its lower central series reaches the trivial subgroup in finitely many steps.

lean4-proofgroup-theoryvisualization

Jordan-Hölder Theorem

Any two composition series of a group have the same length and isomorphic composition factors (in some order).

lean4-proofgroup-theoryvisualization

Semidirect Product

A group extension N ⋊ G where G acts on N by automorphisms, generalizing the direct product.

lean4-proofgroup-theoryvisualization

Second Isomorphism Theorem

For subgroups H and normal N of G, the quotient HN/N is isomorphic to H/(H ∩ N).

lean4-proofgroup-theoryvisualization

Third Isomorphism Theorem

A quotient of quotients collapses to a single quotient: (G/N)/(H/N) ≅ G/H

lean4-proofgroup-theoryvisualization

Correspondence Theorem

Subgroups of G/N are in bijection with subgroups of G containing N, preserving the lattice

lean4-proofgroup-theoryvisualization

Free Group

The free group on a set X is the universal group with generators X and no relations

lean4-proofgroup-theoryvisualization

Group Presentation

Every group can be described by generators and relations via a quotient of a free group

lean4-proofgroup-theoryvisualization

Simple Groups

A simple group has no proper nontrivial normal subgroups; the atoms of group composition

lean4-proofgroup-theoryvisualization

Conjugation Action

Every group acts on itself by conjugation; orbits are conjugacy classes

lean4-proofgroup-theoryvisualization

Alternating Group

The alternating group Aₙ consists of even permutations; it has order n!/2 for n ≥ 2

lean4-proofgroup-theoryvisualization

Dihedral Group

The dihedral group Dₙ describes the symmetries of a regular n-gon; it has order 2n

lean4-proofgroup-theoryvisualization