English
For every index i, the i-th element of the I-basis equals the i-th Smith coefficient times the i-th S-basis vector, after identifying I with a subset of S.
Русский
Для каждого индекса i элемент I-базы равен произведению i-го коэффициента Смита на i-ой вектор базы S после идентификации I как подмножества S.
LaTeX
$$$\\forall i,\\ (\\text{selfBasis } b I hI\\, i) = (\\text{smithCoeffs } b I hI\\, i) \\cdot (\\text{ringBasis } b I hI\\, i)$$$
Lean4
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix; these are the entries of the diagonal matrix. See :
* `Ideal.ringBasis` for the basis on `S`,
* `Ideal.selfBasis` for the basis on `I`,
* `Ideal.selfBasis_def` for the proof that the inclusion map forms a square diagonal matrix.
-/
noncomputable def smithCoeffs (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : ι → R :=
(Ideal.exists_smith_normal_form b I hI).choose_spec.choose
