instMonoidHomClass — Mathlib

English

There is a typeclass instance making LocalizationMap S N behave as a MonoidHomClass from M to N.

Русский

Существет инстанс MonoidHomClass, превращающий LocalizationMap S N в набор отображений моноидом из M в N.

LaTeX

$$$\\text{instance: MonoidHomClass }(S.LocalizationMap N) M N$$$

Lean4

@[to_additive]
instance : MonoidHomClass (LocalizationMap S N) M N
    where
  map_one f := f.toMonoidHom.map_one
  map_mul f := f.toMonoidHom.map_mul

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