Theorems · Theorem · group theory

Subgroup.comap_sup_eq_of_le_range

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

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroup