English
The index of a subgroup H in G, defined as the natural number representing the size of G/H (0 if infinite).
Русский
Индекс подгруппы H в группе G — естественное число, равное размеру множества фактор-группы G/H; если бесконечен, равен 0.
LaTeX
$$$\\mathrm{index}(H) = |G/H|$ (with 0 indicating infinite index).$$
Lean4
/-- If `H` and `K` are subgroups of a group `G`, then `relIndex H K : ℕ` is the index
of `H ∩ K` in `K`. The function returns `0` if the index is infinite. -/
@[to_additive /-- If `H` and `K` are subgroups of an additive group `G`, then `relIndex H K : ℕ`
is the index of `H ∩ K` in `K`. The function returns `0` if the index is infinite. -/
]
noncomputable def relIndex : ℕ :=
(H.subgroupOf K).index
