addHom_ext — Mathlib

English

Two additive homomorphisms from SkewMonoidAlgebra to M are equal if they agree on all singleton elements.

Русский

Два аддитивных гомоморфа от SkewMonoidAlgebra в M равны, если совпадают на всех элементарных одиночках.

LaTeX

$$$$ f = g \text{ if } \forall a,b, f( single a b ) = g( single a b ). $$$$

Lean4

/-- If two additive homomorphisms from `SkewMonoidAlgebra k G ` are equal on each `single a b`,
then they are equal. -/
@[ext high]
theorem addHom_ext {M : Type*} [AddZeroClass M] {f g : SkewMonoidAlgebra k G →+ M}
    (h : ∀ a b, f (single a b) = g (single a b)) : f = g := by ext p;
  induction p using SkewMonoidAlgebra.induction_on <;> simp_all

Похожие утверждения