Theorems · Definition · group theory

Sylow.mulEquivIteratedWreathProduct

(p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    (n : ℕ) →
      (α : Type u_3) →
        [Finite α] →
          Nat.card α = p ^ n →
            (G : Type u_4) →
              [inst : Group G] →
                [Finite G] → Nat.card G = p → (P : Sylow p (Equiv.Perm α)) → ↥↑P ≃* IteratedWreathProduct G n

The encoding of the Sylow p-subgroups of Perm α as an iterated wreath product.

Defined in

Mathlib.GroupTheory.RegularWreathProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactFiniteGroupFinite