Theorems · Theorem · group theory

Sylow.mapSurjective_surjective

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

Defined in

Mathlib.GroupTheory.Sylow

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFiniteGroupFact