addHom_ext' — Mathlib

English

If two additive monoid homomorphisms from SkewMonoidAlgebra k G to an additive zero object N agree after precomposition with every singleAddHom x, then they are equal.

Русский

Если два аддитивных гомоморфа моноидов от SkewMonoidAlgebra k G до N совпадают после предварительной композиции с каждым singleAddHom x, то они равны.

LaTeX

$$$\forall x,\ f(\mathrm{singleAddHom}\ x) = g(\mathrm{singleAddHom}\ x) \implies f = g$$$

Lean4

@[ext high]
theorem addHom_ext' {N : Type*} [AddZeroClass N] ⦃f g : SkewMonoidAlgebra k G →+ N⦄
    (H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g :=
  addHom_ext fun x ↦ DFunLike.congr_fun (H x)

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