index_map_of_injective — Mathlib

English

If f is injective, then (H.map f).index = H.index · f.range.index.

Русский

Если f инъективен, то индекс образа H под f равен произведению индекса H на индекс диапазона f.

LaTeX

$$$ (H.map f).index = H.index \cdot f.range.index. $$$

Lean4

@[to_additive]
theorem index_map_of_injective {f : G →* G'} (hf : Function.Injective f) : (H.map f).index = H.index * f.range.index :=
  by rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]

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