Theorems · Theorem · group theory

Subgroup.comap_le_comap_of_surjective

∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K L : Subgroup N},
  Function.Surjective ⇑f → (Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L)

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupGroup