English
An extensionality principle for MonoidAlgebra homomorphisms: two G-graded linear maps from MonoidAlgebra k G to a target N are equal if they agree after precomposing with every lsingle a (a ∈ G).
Русский
Принцип экстрансиальности для гомоморфизмов MonoidAlgebra: два линейных отображения, совместимые с действием G, совпадают, если при композиции с каждым lsingle a (a ∈ G) они совпадают.
LaTeX
$$$$\\forall\\{N\\},\\ [\\text{MonoidAlgebra } k G \\to+\\!R N],\\ f,g:\\MonoidAlgebra k G \\to_{+}^{[R]} N,\\ (\\forall a\\in G,\; f\\circ (\\text{DistribMulActionHom.single } a) = g\\circ (\\text{DistribMulActionHom.single } a)) \\Rightarrow f=g.$$$$
Lean4
/-- A copy of `Finsupp.distribMulActionHom_ext'` for `MonoidAlgebra`. -/
@[ext]
theorem distribMulActionHom_ext' {N : Type*} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N]
[DistribMulAction R k] {f g : MonoidAlgebra 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
