Theorems · Definition · commutative algebra

LocalizedModule.AtPrime

{R : Type u_1} →
  [inst : CommSemiring R] →
    (P : Ideal R) → [P.IsPrime] → (M : Type u_2) → [inst_2 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)

Given a prime ideal P, LocalizedModule.AtPrime P M is a localization of M at the complement of P.

Defined in: Mathlib.Algebra.Module.LocalizedModule.AtPrime
Cited by: 4 results in Mathlib
Foundations: Depth 31 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Ideal.IsPrime AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Idealstatement and proof · cited by 4,748
Ideal.IsPrimestatement and proof · cited by 827
Ideal.primeComplproof · cited by 462
LocalizedModuleproof · cited by 154

Cited by4

Results whose statement or proof uses this declaration.

IsSMulRegular.subsingleton_linearMap_iffproof · cited by 2
Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimesstatement · cited by 1
Ideal.finrank_fiber_eq_finrankproof · cited by 1
Module.Free.away_of_finite_of_flat_of_rankAtStalk_constantproof · cited by 0