English
If an ideal I factors as a finite product I = ∏_{i∈s} P_i^{e_i} of prime powers, then the quotient ring R/I decomposes as a product of the quotients R/P_i^{e_i}.
Русский
Если идеал I факторизуется как конечное произведение I = ∏_{i∈s} P_i^{e_i} из простых степеней, то кольцо R/I распадается на произведение остальных факторий R/P_i^{e_i}.
LaTeX
$$$I = \prod_{i\in s} P_i^{e_i} \quad\Rightarrow\quad R/I \cong \prod_{i\in s} R/P_i^{e_i}$$$
Lean4
/-- **Chinese remainder theorem** for a Dedekind domain: if the ideal `I` factors as
`∏ i, P i ^ e i`, then `R ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`. -/
noncomputable def quotientEquivPiOfProdEq {ι : Type*} [Fintype ι] (I : Ideal R) (P : ι → Ideal R) (e : ι → ℕ)
(prime : ∀ i, Prime (P i)) (coprime : Pairwise fun i j => P i ≠ P j) (prod_eq : ∏ i, P i ^ e i = I) :
R ⧸ I ≃+* ∀ i, R ⧸ P i ^ e i :=
(Ideal.quotEquivOfEq
(by
simp only [← prod_eq, Finset.inf_eq_iInf, Finset.mem_univ, ciInf_pos,
← IsDedekindDomain.inf_prime_pow_eq_prod _ _ _ (fun i _ => prime i) (coprime.set_pairwise _)])).trans <|
Ideal.quotientInfRingEquivPiQuotient _ fun i j hij =>
Ideal.coprime_of_no_prime_ge <| by
intro P hPi hPj hPp
haveI := Ideal.isPrime_of_prime (prime i)
haveI := Ideal.isPrime_of_prime (prime j)
exact
coprime hij <|
((Ring.DimensionLeOne.prime_le_prime_iff_eq (prime i).ne_zero).mp (hPp.le_of_pow_le hPi)).trans <|
Eq.symm <| (Ring.DimensionLeOne.prime_le_prime_iff_eq (prime j).ne_zero).mp (hPp.le_of_pow_le hPj)
