English
Two elements of MonoidAlgebra R M are equal if they have the same coefficients for every basis element m ∈ M; equivalently, if f(m) = g(m) for all m, then f = g.
Русский
Два элемента MonoidAlgebra R M равны, если совпадают их коэффициенты по каждому базисному элементу m ∈ M; то есть если f(m) = g(m) для всех m, то f = g.
LaTeX
$$$\\forall f,g : MonoidAlgebra(R,M), (\\forall m \\in M, f(m) = g(m)) \\Rightarrow f = g$$$
Lean4
/-- A copy of `Finsupp.ext` for `MonoidAlgebra`. -/
@[to_additive (attr := ext) /-- A copy of `Finsupp.ext` for `AddMonoidAlgebra`. -/
]
theorem ext ⦃f g : MonoidAlgebra R M⦄ (hfg : ∀ m, f m = g m) : f = g :=
Finsupp.ext hfg
