Theorems · Definition · group theory

Sylow.directProductOfNormal

{G : Type u} →
  [inst : Group G] →
    [Finite G] →
      (∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal) →
        ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥P) ≃* G

If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product of these Sylow subgroups.

Defined in

Mathlib.GroupTheory.Sylow

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFinite