Theorems · Theorem · commutative algebra

Ideal.pi_quotient_surjective

∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R},
  Pairwise (Function.onFun IsCoprime I) → ∀ (x : (i : ι) → R ⧸ I i), ∃ r, ∀ (i : ι), (Ideal.Quotient.mk (I i)) r = x i

Corollary of Chinese Remainder Theorem: if Iᵢ are pairwise coprime ideals in a commutative ring then the canonical map R → ∏ (R ⧸ Iᵢ) is surjective.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

2 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFinite