AtPrime — Mathlib

English

Abbrev AtPrime S P denotes the localization of a ring R at the complement of a prime ideal P; i.e., AtPrime S P = IsLocalization P.primeCompl S.

Русский

Условное обозначение AtPrime S P означает локализацию кольца R по дополнению к простому идеалу P; то есть AtPrime S P = IsLocalization P.primeCompl S.

LaTeX

$$$$ \text{AtPrime}(S,P) := \text{IsLocalization } P.{\text{primeCompl}} S $$$$

Lean4

/-- Given a prime ideal `P`, the typeclass `IsLocalization.AtPrime S P` states that `S` is
isomorphic to the localization of `R` at the complement of `P`. -/
protected abbrev AtPrime :=
  IsLocalization P.primeCompl S

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