Theorems · Theorem · group theory

Subgroup.SchurZassenhausInduction.step7

∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G], IsMulCommutative ↥N

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

Defined in

Mathlib.GroupTheory.SchurZassenhaus

Cited by

0 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupSubgroup.NormalFinite