instFunLikeContMDiffMonoidMorphism

English

Every ContMDiffMonoidMorphism preserves multiplication and the unit.

Русский

Каждый ContMDiffMonoidMorphism сохраняет произведение и единицу моноида.

LaTeX

$$$\\\\forall f: ContMDiffMonoidMorphism I I' n G G', \\\\ f(1_G) = 1_{G'}, \\\\forall a,b \\\\in G, \\\\ f(a b) = f(a) f(b)$$$

Lean4

@[to_additive]
instance : FunLike (ContMDiffMonoidMorphism I I' n G G') G G'
    where
  coe a := a.toFun
  coe_injective' f g h := by cases f; cases g; congr; exact DFunLike.ext' h

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