English
Given residues x_i in R/(P_i^{e_i}) for i in a finite set, there exists y in R representing all of them simultaneously modulo each P_i^{e_i}.
Русский
Даны остатки x_i в R/(P_i^{e_i}) для i из конечного множества, существует y в R, который совместимо представляет их modulo каждое P_i^{e_i}.
LaTeX
$$There exists y ∈ R such that ∀ i ∈ s, y ≡ x_i (mod P_i^{e_i})$$
Lean4
/-- Corollary of the Chinese remainder theorem: given elements `x i : R / P i ^ e i`,
we can choose a representative `y : R` such that `y ≡ x i (mod P i ^ e i)`. -/
theorem exists_representative_mod_finset {ι : 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 : ∀ i : s, R ⧸ P i ^ e i) :
∃ y, ∀ (i) (hi : i ∈ s), Ideal.Quotient.mk (P i ^ e i) y = x ⟨i, hi⟩ :=
by
let f := IsDedekindDomain.quotientEquivPiOfFinsetProdEq _ P e prime coprime rfl
obtain ⟨y, rfl⟩ := f.surjective x
obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective y
exact ⟨z, fun i _hi => rfl⟩
