Away — Mathlib

English

The Away construction provides a well-behaved inverse for the adjoinRoot localization.

Русский

Конструкция Away обеспечивает корректную обратимость для локализации AdjoinRoot.

LaTeX

$$IsLocalization.Away.invSelf x$$

Lean4

/-- Given `x : R`, the typeclass `IsLocalization.Away x S` states that `S` is
isomorphic to the localization of `R` at the submonoid generated by `x`.
See `IsLocalization.Away.mk` for a specialized constructor. -/
abbrev Away (S : Type*) [CommSemiring S] [Algebra R S] :=
  IsLocalization (Submonoid.powers x) S

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