Theorems · Theorem · commutative algebra

LocalizedModule.exists_subsingleton_away

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (p : Ideal R) [inst_4 : p.IsPrime] [Subsingleton (LocalizedModule p.primeCompl M)],
  ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

If M is a finite module such that Mₚ = 0 for some p, then M[1/f] = 0 for some p ∈ D(f).

Defined in

Mathlib.RingTheory.Support

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModule.FiniteIdeal.IsPrimeSubsingleton