English
There exist a basis b' for S, a coefficient function a, and a basis ab' for I such that each I-vector is a scalar multiple of the corresponding S-vector, expressing a diagonal inclusion.
Русский
Существуют база b' для S, функция коэффициентов a и база ab' для I, таких что каждый вектор I является скалярным множителем соответствующего вектора S, задавая диагональное включение.
LaTeX
$$$\\exists b', a, ab'\\;\\forall i,\\ (ab' i : S) = a i \\cdot b' 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.
-/
@[simp]
theorem selfBasis_def (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) :
∀ i, (Ideal.selfBasis b I hI i : S) = Ideal.smithCoeffs b I hI i • Ideal.ringBasis b I hI i :=
(Ideal.exists_smith_normal_form b I hI).choose_spec.choose_spec.choose_spec
