Theorems · Definition · group theory

Sylow.mapSurjective

{p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      [Finite G] →
        {G' : Type u_2} →
          [inst_2 : Group G'] → {f : G →* G'} → Function.Surjective ⇑f → [Fact (Nat.Prime p)] → Sylow p G → Sylow p G'

Surjective group homomorphisms map Sylow subgroups to Sylow subgroups.

Defined in

Mathlib.GroupTheory.Sylow

Cited by

4 results in Mathlib

Foundations

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

Assumes

GroupFiniteGroupFact