English
There is a canonical identification between the canonical function-coercion of MonoidAlgebra R M and the corresponding Finsupp-based coercion to functions M → R; i.e., the way MonoidAlgebra elements act as functions on M agrees with the standard FinSupp representation.
Русский
Существует каноническое соответствие между выходной функцией MonoidAlgebra R M и соответствующим отображением через Finsupp в функции M → R; то есть квадрат коэрции MonoidAlgebra на функции согласуется с обычным представлением через Finsupp.
LaTeX
$$$\\mathrm{coe}_{MonoidAlgebra} = \\mathrm{coe}_{Finsupp} : MonoidAlgebra(R,M) \\to (M \\to R)$$$
Lean4
@[to_additive]
instance instCoeFun : CoeFun (MonoidAlgebra R M) fun _ ↦ M → R :=
inferInstanceAs <| CoeFun (M →₀ R) fun _ ↦ M → R
