instFunLike — Mathlib

English

LocalizationMap S N carries a canonical FunLike structure, i.e., it can be treated as a function from M to N with coherence of compositions.

Русский

LocalizationMap S N обладает структурой FunLike; его можно рассматривать как функцию M → N со свойствами совместимости композиции.

LaTeX

$$$\\text{LocalizationMap}$ is a FunLike object: $(f: S.LocalizationMap N)\\to (M\\to N)$ with coherence.$$

Lean4

@[to_additive]
instance : FunLike (LocalizationMap S N) M N where
  coe f := f.toMonoidHom
  coe_injective' := DFunLike.coe_injective.comp toMonoidHom_injective

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