awayMap — Mathlib

English

Given a map f: R →+* P, one obtains a corresponding map from Localization.Away r to Localization.Away (f r).

Русский

Для отображения f: R →+* P существует соответствующее отображение между Away r и Away (f r).

LaTeX

$$$\mathrm{awayMap}(f) : \operatorname{Away\} r \to+* \operatorname{Away}(f r)$$$

Lean4

/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/
noncomputable abbrev awayMap (f : R →+* P) (r : R) : Localization.Away r →+* Localization.Away (f r) :=
  IsLocalization.Away.map _ _ f r

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