toMap — Mathlib

English

Abbreviation that extracts the underlying monoid hom from a localization map, viewing it as a function.

Русский

Сокращение, извлекающее базовый моноид-гомоморфизм из локализационной карты.

LaTeX

$$$\\mathrm{toMap}(f) = f.toMonoidHom$.$$

Lean4

/-- Short for `toMonoidHom`; used to apply a localization map as a function. -/
@[to_additive /-- Short for `toAddMonoidHom`; used to apply a localization map as a function. -/
    ]
abbrev toMap (f : LocalizationMap S N) :=
  f.toMonoidHom

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