snd_comp_quotientInfEquivQuotientProd

English

Two coprime ideals I, J give a ring isomorphism R/(I ⊓ J) ≅ (R/I) × (R/J); equivalently, the Chinese Remainder Theorem specialized to multiplication.

Русский

Два взаимно простых идеала I, J дают изоморфизм кольца R/(I ⊓ J) ≅ (R/I) × (R/J); это частный случай CRT для умножения.

LaTeX

$$$R/(I \cap J) \cong (R/I) \times (R/J)$ under coprime I, J$$

Lean4

@[simp]
theorem snd_comp_quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.snd _ _).comp (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor inf_le_right :=
  by apply Quotient.ringHom_ext; ext; rfl

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