20 Group theory and generalizations

TheoremCauchy's theorem (group theory)#

For every prime p dividing the order of a finite group G there exists an element of order p in G. This is known as Cauchy's theorem.

exists_prime_orderOf_dvd_card.{u_3} {G : Type u_3} [Group G] [Fintype G] (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hdvd : p ∣ Fintype.card G) : ∃ x, orderOf x = p
Sources
Mathlibexists_prime_orderOf_dvd_card
Uses 7 · Used by 1
Statement usesFinite set · Integer · Irreducible element · Order of an element
Proof usesDecomposition into cycles with disjoint support · Greatest common divisor · Least common multiple
Used byFirst Sylow theorem

TheoremJordan–Hölder theorem#

The Jordan-Hölder theorem, stated for any JordanHolderLattice. If two composition series start and finish at the same place, they are equivalent.

CompositionSeries.jordan_holder.{u} {X : Type u} [Lattice X] [JordanHolderLattice X]
  (s₁ s₂ : CompositionSeries X) (hb : RelSeries.head s₁ = RelSeries.head s₂)
  (ht : RelSeries.last s₁ = RelSeries.last s₂) : s₁.Equivalent s₂
Sources
MathlibCompositionSeries.jordan_holder
Uses 4
Statement usesNatural number
Proof usesFinite set · Integer · Permutation group of a type

TheoremNielsen–Schreier theorem#

The Nielsen-Schreier theorem: a subgroup of a free group is free.

Subgroup.isFreeGroupOfIsFreeGroup.{u} {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) :
  IsFreeGroup ↥H
Sources
MathlibSubgroup.isFreeGroupOfIsFreeGroup
Uses 7
Statement usesFree group · Integer · Subgroup
Proof usesIsomorphism · List · Orbit · Small category

TheoremSchur's lemma (1000+ theorems)#

Schur's lemma for endomorphisms in 𝕜-linear categories.

CategoryTheory.finrank_endomorphism_simple_eq_one.{v_1, u_1, u_2} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜]
  [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C)
  [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] : Module.finrank 𝕜 (X ⟶ X) = 1
Sources
MathlibCategoryTheory.finrank_endomorphism_simple_eq_one
Uses 8 · Used by 1
Statement usesAlgebraically closed field · Cardinal · Finite-dimensionality · Limits · Linear independence · Small category
Proof usesAssociative algebra over a commutative ring · Local ring
Used bySchur's lemma (Linear representations)

TheoremSchur–Zassenhaus theorem#

Schur-Zassenhaus for normal subgroups: If H : Subgroup G is normal, and has order coprime to its index, then there exists a subgroup K which is a (left) complement of H.

Subgroup.exists_left_complement'_of_coprime.{u} {G : Type u} [Group G] {N : Subgroup G} [N.Normal]
  (hN : (Nat.card ↥N).Coprime N.index) : ∃ H, H.IsComplement' N
Sources
MathlibSubgroup.exists_left_complement'_of_coprime
Uses 7
Statement usesCardinal · Index of a subgroup · Integer · Normal subgroup · Ring morphism
Proof usesEuclid's' algorithm · Third Sylow theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.