instOneContMDiffMonoidMorphism — Mathlib

English

There exists a canonical identity ContMDiffMonoidMorphism from G to G' sending every element to the unit element.

Русский

Существует каноническое единичное отображение ContMDiffMonoidMorphism из G в G', отправляющее каждый элемент в единицу.

LaTeX

$$One (ContMDiffMonoidMorphism I I' n G G')$$

Lean4

@[to_additive]
instance : One (ContMDiffMonoidMorphism I I' n G G') :=
  ⟨{  contMDiff_toFun := contMDiff_const
      toMonoidHom := 1 }⟩

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