relIndex_ker — Mathlib

English

For a subgroup K ≤ G, the relative index of ker f with respect to K equals the cardinality of K.map f.

Русский

Для подгруппы K ≤ G относительный индекс ядра f относительно K равен мощности образа K под f.

LaTeX

$$$ f.ker.\mathrm{relIndex}(K) = |K.map f|. $$$

Lean4

@[to_additive]
theorem relIndex_ker (f : G →* G') : f.ker.relIndex K = Nat.card (K.map f) := by
  rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]

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