English
The extensionality principle for AddMonoidAlgebra linear maps, mirroring the MonoidAlgebra version: equality is determined by behavior on lsingle x for all x.
Русский
Принцип экстрансиальности для линейных отображений AddMonoidAlgebra, аналогично версии для MonoidAlgebra: равенство определяется по поведению на lsingle x для всех x.
LaTeX
$$$$\forall f,g:\ AddMonoidAlgebra k G \to+[R] N,\ (\forall x:\, G,\ f\circ (AddMonoidAlgebra.lsingle x) = g\circ (AddMonoidAlgebra.lsingle x)) \Rightarrow f=g.$$$$
Lean4
/-- A copy of `Finsupp.lhom_ext'` for `AddMonoidAlgebra`. -/
@[ext high]
theorem lhom_ext' {N : Type*} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k]
⦃f g : AddMonoidAlgebra k G →ₗ[R] N⦄ (H : ∀ (x : G), LinearMap.comp f (lsingle x) = LinearMap.comp g (lsingle x)) :
f = g :=
Finsupp.lhom_ext' H
