English
Given a S-ideal I and a basis b of S over R with I ≠ ⊥, the quotient S/I is canonically R-linear isomorphic to the product over i of R modulo the span of the Smith coefficient I.smithCoeffs(b,hI,i).
Русский
При Im I и базисе b над S, с условием I ≠ ⊥, площадь S/I изоморфна как R-модуль произведению по i модулей R / span{ I.smithCoeffs(b,hI,i) }.
LaTeX
$$$(S/I) \cong_R \prod_{i} \left(R/\langle I.smithCoeffs\, b\, hI\, i\rangle\right)$$$
Lean4
/-- We can write the quotient of an ideal over a PID as a product of quotients by principal ideals.
-/
noncomputable def quotientEquivPiSpan (I : Ideal S) (b : Basis ι R S) (hI : I ≠ ⊥) :
(S ⧸ I) ≃ₗ[R] ∀ i, R ⧸ span ({I.smithCoeffs b hI i} : Set R) :=
Submodule.quotientEquivPiSpan (I.restrictScalars R) b <| finrank_eq_finrank b I hI
