English
For a scalar x in R and a linear map f: M →ₗ[R] M', IsLocalizedModule.Away x f describes the localization of M at the submonoid generated by x.
Русский
Для скаляра x в R и линейного отображения f: M →ₗ[R] M' конструкция Away x f описывает локализацию M по подмонойду, порождаемому x.
LaTeX
$$$\\text{Away}_x f \\;\\cong\\; \\operatorname{Loc}_{\\langle x \\rangle}(M)$.$$
Lean4
/-- Given `x : R` and `f : M →ₗ[R] M'`, IsLocalization.Away x f` states that `M'`
is isomorphic to the localization of `M` at the submonoid generated by `x`. -/
protected abbrev Away {R M M' : Type*} [CommSemiring R] (x : R) [AddCommMonoid M] [Module R M] [AddCommMonoid M']
[Module R M'] (f : M →ₗ[R] M') :=
IsLocalizedModule (Submonoid.powers x) f
