English
A finite subproduct of prime powers yields the same quotient decomposition, mirroring the infinite product case but restricted to a finite index set.
Русский
Конечное подпроизведение простых степеней даёт такое же разложение по факториалам, как и бесконечный случай, но для конечного индекса.
LaTeX
$$If I = ∏_{i∈s} P_i^{e_i}, then R/I ≅ ∀ i∈s, R/P_i^{e_i}$$
Lean4
/-- **Chinese remainder theorem** for a Dedekind domain: if the ideal `I` factors as
`∏ i ∈ s, P i ^ e i`, then `R ⧸ I` factors as `Π (i : s), R ⧸ (P i ^ e i)`.
This is a version of `IsDedekindDomain.quotientEquivPiOfProdEq` where we restrict
the product to a finite subset `s` of a potentially infinite indexing type `ι`.
-/
noncomputable def quotientEquivPiOfFinsetProdEq {ι : Type*} {s : Finset ι} (I : Ideal R) (P : ι → Ideal R) (e : ι → ℕ)
(prime : ∀ i ∈ s, Prime (P i)) (coprime : ∀ᵉ (i ∈ s) (j ∈ s), i ≠ j → P i ≠ P j)
(prod_eq : ∏ i ∈ s, P i ^ e i = I) : R ⧸ I ≃+* ∀ i : s, R ⧸ P i ^ e i :=
IsDedekindDomain.quotientEquivPiOfProdEq I (fun i : s => P i) (fun i : s => e i) (fun i => prime i i.2)
(fun i j h => coprime i i.2 j j.2 (Subtype.coe_injective.ne h))
(_root_.trans (Finset.prod_coe_sort s fun i => P i ^ e i) prod_eq)
