relIndex_map_map — Mathlib

English

If K is normal, then relIndex (H ⊔ K) in K equals relIndex H in K.

Русский

Если K нормальная, то relIndex (H ⊔ K) в K равно relIndex H в K.

LaTeX

$$$\\mathrm{relIndex}(K, H ⊔ K) = \\mathrm{relIndex}(K, H).$$$

Lean4

@[to_additive]
theorem relIndex_map_map (f : G →* G') (H K : Subgroup G) :
    (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker) := by
  rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]

Похожие утверждения