relIndex_comap — Mathlib

English

If f: G →* G' is an injective homomorphism, then relIndex (map f H) (map f K) = relIndex H K.

Русский

Если f: G →* G' инъективен, то relIndex (map f H) (map f K) = relIndex H K.

LaTeX

$$$\\mathrm{relIndex}(\\mathrm{map}\ f\ H, \\mathrm{map}\ f\ K) = \\mathrm{relIndex}(H, K)$, under injectivity of f.$$

Lean4

@[to_additive]
theorem relIndex_comap (f : G' →* G) (K : Subgroup G') : relIndex (comap f H) K = relIndex H (map f K) := by
  rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]

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