eq_zero_of_localization — Mathlib

English

If the image of r is zero in every prime localization, then r = 0.

Русский

Если образ r равен нулю во всех локализациях поprime, то r = 0.

LaTeX

$$$\\forall J\\ (J\\text{ maximal}),\\; \\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(J)}(r) = 0 \\Rightarrow r = 0$$

Lean4

theorem eq_zero_of_localization (r : R)
    (h : ∀ (J : Ideal R) (_ : J.IsMaximal), algebraMap R (Localization.AtPrime J) r = 0) : r = 0 :=
  Module.eq_zero_of_localization_maximal _ (fun _ _ ↦ Algebra.linearMap R _) r h

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