English
Let b be a basis for M over Z and bN a basis for N over Z of the same dimension. Then the determinant of b with respect to bN has natAbs equal to the cardinality of M/N.
Русский
Пусть b — базис M над Z, bN — базис N над Z той же размерности. Тогда детерминант b относительно bN имеет natAbs, равное кардинальности M/N.
LaTeX
$$$$ (b.det (N.subtype \circ bN)).natAbs = \mathrm{card}(M / N). $$$$
Lean4
/-- Quotients by submodules of full rank of free finite `ℤ`-modules are isomorphic
to a direct product of `ZMod`.
-/
noncomputable def quotientEquivPiZMod (N : Submodule ℤ M) (b : Basis ι ℤ M)
(h : Module.finrank ℤ N = Module.finrank ℤ M) : M ⧸ N ≃+ Π i, ZMod (smithNormalFormCoeffs b h i).natAbs :=
let a := smithNormalFormCoeffs b h
let e := N.quotientEquivPiSpan b h
let e' : (∀ i : ι, ℤ ⧸ Ideal.span ({a i} : Set ℤ)) ≃+ ∀ i : ι, ZMod (a i).natAbs :=
AddEquiv.piCongrRight fun i => ↑(Int.quotientSpanEquivZMod (a i))
(↑(e : (M ⧸ N) ≃ₗ[ℤ] _) : M ⧸ N ≃+ _).trans e'
