ideal_eq_bot_of_localization' — Mathlib

English

An ideal is zero if its localization at every maximal ideal is zero.

Русский

Идеал нулевой, если его локализация в каждом максимальном идеале нулевая.

LaTeX

$$$I = \\mathbf{0} \\quad\\text{iff}\\quad \\forall \\text{ maximal }J,\\; \\mathrm{Ideal.map}(\\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(J)})\,I = 0$$

Lean4

/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/
theorem ideal_eq_bot_of_localization' (I : Ideal R)
    (h : ∀ (J : Ideal R) (_ : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) : I = ⊥ :=
  Ideal.eq_of_localization_maximal fun P hP => by simpa using h P hP

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