constMonoidHom — Mathlib

English

There is a monoid hom from Y to LocallyConstant(X,Y) sending y to the constant function with value y.

Русский

Существует моноид-гомоморфизм от Y к LocallyConstant(X,Y), отправляющий y в константную функцию, которая принимает значение y.

LaTeX

$$constMonoidHom(y)(x) = y for all x$$

Lean4

/-- The constant-function embedding, as a multiplicative monoid hom. -/
@[to_additive (attr := simps) /-- The constant-function embedding, as an additive monoid hom. -/
    ]
def constMonoidHom [MulOneClass Y] : Y →* LocallyConstant X Y
    where
  toFun := const X
  map_one' := rfl
  map_mul' _ _ := rfl

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