coeFnMonoidHom — Mathlib

English

There is a monoid hom from LocallyConstant(X,Y) to X → Y given by the function-into-mapping, i.e., taking the underlying function is compatible with monoid structure.

Русский

Существует гомоморф Моноида от LocallyConstant(X,Y) к X → Y, задаваемый отображением к его естественной функции.

LaTeX

$$\text{coeFnMonoidHom} : LocallyConstant(X,Y) \to_* (X \to Y)$$

Lean4

/-- `DFunLike.coe` as a `MonoidHom`. -/
@[to_additive (attr := simps) /-- `DFunLike.coe` as an `AddMonoidHom`. -/
    ]
def coeFnMonoidHom [MulOneClass Y] : LocallyConstant X Y →* X → Y
    where
  toFun := DFunLike.coe
  map_one' := rfl
  map_mul' _ _ := rfl

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