English
The element supported at m with coefficient r is given by single m r; it has value r at m and zero elsewhere.
Русский
Элемент, поддерживаемый в позиции m с коэффициентом r, задаётся как single m r; он имеет значение r в m и нули в остальных местах.
LaTeX
$$$\\mathrm{single}(m,r) \\in MonoidAlgebra(R,M)$ is the basis element with support {m} and coefficient r, i.e. $(\\mathrm{single}(m,r))(m') = \\begin{cases} r, & m'=m, \\\\ 0, & m'\\neq m. \\end{cases}$$$
Lean4
/-- `MonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : MonoidAlgebra R M`. -/
@[to_additive /-- `AddMonoidAlgebra.single m r` for `m : M`, `r : R` is the element `rm : R[M]`. -/
]
abbrev single (m : M) (r : R) : MonoidAlgebra R M :=
Finsupp.single m r
