Theorems · Definition · commutative algebra

Ideal.quotientInfRingEquivPiQuotient

• 1000+ list: Chinese remainder theorem

{R : Type u_2} →
  [inst : CommRing R] →
    {ι : Type u_3} →
      [Finite ι] → (f : ι → Ideal R) → Pairwise (Function.onFun IsCoprime f) → R ⧸ ⨅ i, f i ≃+* ((i : ι) → R ⧸ f i)

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingFinite