English
A copy of the extensionality lemma for MonoidAlgebra morphisms with distributive action, identifying equality by action on lsingle a.
Русский
Копия леммы экстрансиальности для отображений MonoidAlgebra с дистрибьюторским действием, идентифицирующая равенство по действию на lsingle a.
LaTeX
$$$$\forall f,g:\ MonoidAlgebra k G \to+[R] N,\ (\forall a:\, G,\ f\circ (DistribMulActionHom.single a) = g\circ (DistribMulActionHom.single a)) \Rightarrow f=g.$$$$
Lean4
/-- A copy of `Finsupp.distribMulActionHom_ext'` for `AddMonoidAlgebra`. -/
@[ext]
theorem distribMulActionHom_ext' {N : Type*} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N]
[DistribMulAction R k] {f g : AddMonoidAlgebra k G →+[R] N}
(h : ∀ a : G, f.comp (DistribMulActionHom.single (M := k) a) = g.comp (DistribMulActionHom.single a)) : f = g :=
Finsupp.distribMulActionHom_ext' h
