quotientEquivPiZMod — Mathlib

English

If I ≠ ⊥, then S/I is linearly isomorphic (as an additive group) to the product over i of ZMod(I.smithCoeffs(b,hI,i).natAbs).

Русский

При I ≠ ⊥, фактор-модуль S/I изоморфен как аддитивная группа произведению ZMod( natAbs(I.smithCoeffs(b,hI,i)) ) по i.

LaTeX

$$(S/I) ≃_+ ∀ i, ZMod((I.smithCoeffs b hI i).natAbs)$$

Lean4

/-- Ideal quotients over a free finite extension of `ℤ` are isomorphic to a direct product of
`ZMod`. -/
noncomputable def quotientEquivPiZMod (I : Ideal S) (b : Basis ι ℤ S) (hI : I ≠ ⊥) :
    S ⧸ I ≃+ ∀ i, ZMod (I.smithCoeffs b hI i).natAbs :=
  Submodule.quotientEquivPiZMod (I.restrictScalars ℤ) b <| finrank_eq_finrank b I hI

Похожие утверждения