quotientInfEquivQuotientProd_fst — Mathlib

English

There is a ring isomorphism between R/(⋂ i I_i) and ∏ i R/I_i when ideals are pairwise coprime.

Русский

Существует изоморфизм колец между R/(⋂ I_i) и ∏ i R/I_i при попарной взаимной простоте I_i.

LaTeX

$$$\text{quotientInfRingEquivPiQuotient } I$$$

Lean4

@[simp]
theorem quotientInfEquivQuotientProd_fst (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) :
    (quotientInfEquivQuotientProd I J coprime x).fst = Ideal.Quotient.factor inf_le_left x :=
  Quot.inductionOn x fun _ => rfl

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