English
The index of the Smith form submodule is nonzero if and only if the submodule basis has exactly as many vectors as the module basis (n = card ι).
Русский
Индекс не нулевой тогда и только тогда, когда число векторов в подбазе Смит совпадает с размерностью модуля: n = card ι.
LaTeX
$$$N.toAddSubgroup.index \neq 0 \iff n = |\iota|$$$
Lean4
/-- Given a submodule `N` in Smith normal form of a free ℤ-module, it has finite index as an
additive subgroup (i.e., `N.toAddSubgroup.index ≠ 0`) if and only if the submodule basis has as
many vectors as the basis for the module. -/
theorem toAddSubgroup_index_ne_zero_iff {N : Submodule ℤ M} (snf : Basis.SmithNormalForm N ι n) :
N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι :=
by
rw [snf.toAddSubgroup_index_eq_ite]
rcases snf with ⟨bM, bN, f, a, snf⟩
simp only [ne_eq, ite_eq_right_iff, Classical.not_imp, and_iff_left_iff_imp]
have ha : ∀ i, a i ≠ 0 := by
intro i hi
apply Basis.ne_zero bN i
specialize snf i
simpa [hi] using snf
intro h
simpa [Ideal.span_singleton_toAddSubgroup_eq_zmultiples, Int.index_zmultiples, Finset.prod_eq_zero_iff] using ha
