exists_forall_sub_mem_ideal — Mathlib

English

Under coprimality, for any family of elements x_i, there exists r ∈ R with r − x_i ∈ I_i for all i.

Русский

При условии взаимной простоты существует r ∈ R такой, что r − x_i ∈ I_i для всех i.

LaTeX

$$$\exists r:\\ R, \forall i, r - x_i \in I_i$$$

Lean4

/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then given elements `xᵢ` you can find `r` with `r - xᵢ ∈ Iᵢ` for all `i`. -/
theorem exists_forall_sub_mem_ideal {I : ι → Ideal R} (hI : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : ι → R) :
    ∃ r : R, ∀ i, r - x i ∈ I i :=
  by
  obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)
  exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Похожие утверждения