English
A finite CRT construction yields a ring isomorphism between R/I and the product over i in a finite set s of R/(P_i^{e_i}).
Русский
Конструкция CRT для конечного множества даёт изоморфизм кольца между R/I и произведением по i∈s R/(P_i^{e_i}).
LaTeX
$$IsDedekindDomain quotientEquivPiOfFinsetProdEq I P e prime coprime prod_eq : R/I ≃+* ∀ i ∈ s, R/P_i^{e_i}$$
Lean4
/-- Corollary of the Chinese remainder theorem: given elements `x i : R`,
we can choose a representative `y : R` such that `y - x i ∈ P i ^ e i`. -/
theorem exists_forall_sub_mem_ideal {ι : Type*} {s : Finset ι} (P : ι → Ideal R) (e : ι → ℕ)
(prime : ∀ i ∈ s, Prime (P i)) (coprime : ∀ᵉ (i ∈ s) (j ∈ s), i ≠ j → P i ≠ P j) (x : s → R) :
∃ y, ∀ (i) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i :=
by
obtain ⟨y, hy⟩ :=
IsDedekindDomain.exists_representative_mod_finset P e prime coprime fun i => Ideal.Quotient.mk _ (x i)
exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩
