Documentation

Mathlib.GroupTheory.SchurZassenhaus

The Schur-Zassenhaus Theorem #

In this file we prove the Schur-Zassenhaus theorem.

Main results #

The quotient of the transversals of an abelian normal N by the diff relation.

Instances For
    theorem Subgroup.eq_one_of_smul_eq_one {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] [Subgroup.Normal H] (hH : Nat.Coprime (Nat.card { x // x H }) (Subgroup.index H)) (α : Subgroup.QuotientDiff H) (h : { x // x H }) :
    h α = αh = 1

    Proof of the Schur-Zassenhaus theorem #

    In this section, we prove the Schur-Zassenhaus theorem. The proof is by contradiction. We assume that G is a minimal counterexample to the theorem.

    We will arrive at a contradiction via the following steps:

    theorem Subgroup.SchurZassenhausInduction.step7 {G : Type u} [Group G] [Fintype G] {N : Subgroup G} [Subgroup.Normal N] (h1 : Nat.Coprime (Fintype.card { x // x N }) (Subgroup.index N)) (h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'], Fintype.card G' < Fintype.card G∀ {N' : Subgroup G'} [inst_2 : Subgroup.Normal N'], Nat.Coprime (Fintype.card { x // x N' }) (Subgroup.index N')H', Subgroup.IsComplement' N' H') (h3 : ∀ (H : Subgroup G), ¬Subgroup.IsComplement' N H) :

    Do not use this lemma: It is made obsolete by exists_right_complement'_of_coprime

    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 (right) complement of H.

    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 (right) complement of H.

    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.

    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.