quotientInfEquivQuotientProd — Mathlib

English

Under pairwise coprimality, the quotient Inf to Pi quotient is surjective.

Русский

При попарной взаимной простоте образующая функция quotientInfToPiQuotient сюръективна.

LaTeX

$$$\text{quotientInfToPiQuotient_surj } I$$$

Lean4

/-- **Chinese remainder theorem**, specialized to two ideals. -/
noncomputable def quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    R ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J :=
  let f : Fin 2 → Ideal R := ![I, J]
  have hf : Pairwise (IsCoprime on f) := by
    intro i j h
    fin_cases i <;> fin_cases j <;> try contradiction
    · assumption
    · exact coprime.symm
  (Ideal.quotEquivOfEq (by simp [f, iInf, inf_comm])).trans <|
    (Ideal.quotientInfRingEquivPiQuotient f hf).trans <| RingEquiv.piFinTwo fun i => R ⧸ f i

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