Theorems · Theorem · commutative algebra

Ideal.le_ker_atPrime_of_forall_exists_eq_mul

∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  (∀ x ∈ I, ∃ y ∈ I, x = x * y) →
    ∀ {p : Ideal R} [inst_1 : p.IsPrime], I ≤ p → I ≤ RingHom.ker (algebraMap R (Localization.AtPrime p))

[Stacks Tag 04PS](https://stacks.math.columbia.edu/tag/04PS) ((5) => (7))

Defined in

Mathlib.RingTheory.Ideal.Pure

Cited by

1 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Quot.sound

Assumes

CommRingIdeal.IsPrime