Away — Mathlib

English

Away x M is the localization of M at the submonoid generated by x.

Русский

Away x M — локализация M по подмонойду, порождаемому x.

LaTeX

$$$\\text{Away}(x, M) = \\operatorname{Loc}_{\\langle x \\rangle}(M).$$$

Lean4

/-- Given `x : R`, `LocalizedModule.Away x M` is the localization of `M` at the
  submonoid generated by `x`. -/
protected abbrev Away {R : Type*} [CommSemiring R] (x : R) (M : Type*) [AddCommMonoid M] [Module R M] :=
  LocalizedModule (Submonoid.powers x) M

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