English
The multiplication unit of the MonoidAlgebra is given by the basis element at 1 with coefficient 1: one = single 1 1.
Русский
Единицей умножения в MonoidAlgebra является базисный элемент в позиции 1 с коэффициентом 1: one = single 1 1.
LaTeX
$$$\\text{one} : MonoidAlgebra(R,M)\\text{ satisfies } 1 = \\mathrm{single}(1,1)$$$
Lean4
/-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere. -/
@[to_additive (dont_translate := R) /-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere. -/
]
instance one : One (MonoidAlgebra R M) where one := single 1 1
