English
The index formula can be written as an if-then: infinite (zero) when n < card(ι) and otherwise the product formula holds when n equals the full basis cardinal.
Русский
Индекс задаётся ветвлением: бесконечный (нулевой) при n меньше чемcard(ι) и иначе произведение индексов при совпадении с полной базисной размерностью.
LaTeX
$$$N.toAddSubgroup.index = \begin{cases} \prod_{i} (\operatorname{index}\langle a_i \rangle) & \text{if } n=|ι|, \\ 0 & \text{otherwise}. \end{cases}$$$
Lean4
/-- Given a submodule `N` in Smith normal form of a free `R`-module, its index as an additive
subgroup is infinite (represented as zero) if the submodule basis has fewer vectors than the basis
for the module, and otherwise equals the product of the indexes of the ideals generated by each
basis vector. -/
theorem toAddSubgroup_index_eq_ite [Infinite R] [Module R M] {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) :
N.toAddSubgroup.index =
(if n = Fintype.card ι then ∏ i : Fin n, (Ideal.span {snf.a i}).toAddSubgroup.index else 0) :=
by
rw [snf.toAddSubgroup_index_eq_pow_mul_prod]
split_ifs with h
· simp [h]
· have hlt : n < Fintype.card ι := Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
simp [hlt]
