Theorems · Theorem · commutative algebra

Ideal.mem_of_localization_maximal

∀ {R : Type u_1} [inst : CommSemiring R] {r : R} {J : Ideal R},
  (∀ (P : Ideal R) (x : P.IsMaximal),
      (algebraMap R (Localization.AtPrime P)) r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
    r ∈ J

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

2 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring