mk' — Mathlib

English

The fraction m/s with respect to the localization map f is an element mk' f m s of the localized module.

Русский

Дробь m/s относительно отображения локализации f является элементом mk' f m s локализованного модуля.

LaTeX

$$$mk' f m s = fromLocalizedModule(S,f)(LocalizedModule.mk m s) $$$

Lean4

/-- `mk' f m s` is the fraction `m/s` with respect to the localization map `f`. -/
noncomputable def mk' (m : M) (s : S) : M' :=
  fromLocalizedModule S f (LocalizedModule.mk m s)

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