AtPrime — Mathlib

English

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

Русский

Пусть P — простой идеал; LocalizedModule.AtPrime P M дает локализацию M по дополнению к P.

LaTeX

$$$\\text{LocalizedModule.AtPrime}(P, M) \\cong S^{-1}M\\quad (S = R \\setminus P).$$$

Lean4

/-- Given a prime ideal `P`, `LocalizedModule.AtPrime P M` is a localization of `M`
  at the complement of `P`. -/
protected abbrev AtPrime {R : Type*} [CommSemiring R] (P : Ideal R) [P.IsPrime] (M : Type*) [AddCommMonoid M]
    [Module R M] :=
  LocalizedModule P.primeCompl M

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