Theorems · Theorem · group theory

Subgroup.map_injective_of_ker_le

∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) {H K : Subgroup G},
  f.ker ≤ H → f.ker ≤ K → Subgroup.map f H = Subgroup.map f K → H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupGroup