index_map — Mathlib

English

For f: G →* G' the index of H.map f equals the index of H scaled by the index of the range, i.e., (H.map f).index = (H ⊔ ker f).index · range.index.

Русский

Для f: G →* G' индекс изображения H под f равен произведению индекса H и индекса диапазона, т.е. (H.map f).index = (H ⊔ ker f).index · range.index.

LaTeX

$$$ (H.map f).index = (H \lor \ker f).index \cdot (\mathrm{range}(f)).index. $$$

Lean4

@[to_additive]
theorem index_map (f : G →* G') : (H.map f).index = (H ⊔ f.ker).index * f.range.index := by
  rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]

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