Away — Mathlib

English

The homogeneous localization at a prime is a local ring; every nonunit is contained in a unique maximal ideal.

Русский

Однородная локализация по простому является локальным кольцом: любую неединицу можно разместить в единственном максимальном идеале.

LaTeX

$$$$ \text{IsLocalRing}(\mathrm{HomogeneousLocalization.AtPrime}(\mathcal{A}, \mathfrak{p})). $$$$

Lean4

/-- Localizing away from powers of `f` homogeneously. -/
abbrev Away :=
  HomogeneousLocalization 𝒜 (Submonoid.powers f)

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