instOne — Mathlib

English

If Y is a monoid with identity, then LocallyConstant X Y has a natural multiplicative identity given by the constant function 1.

Русский

Пусть Y — моноид с нейтральным элементом, тогда LocallyConstant(X,Y) имеет естественный нейтральный элемент умножения, задаваемый константной функцией 1.

LaTeX

$$$\text{One}$-structure on $\operatorname{LocallyConstant}(X,Y)$ with $1 = \mathrm{const}(X,1).$$$

Lean4

@[to_additive]
instance [One Y] : One (LocallyConstant X Y) where one := const X 1

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