distribMulActionHom_ext — Mathlib

English

Two DistribMulAction homomorphisms f,g from SkewMonoidAlgebra M α to N are equal if they agree on all images of single a m.

Русский

Два гомоморфизма DistribMulAction из SkewMonoidAlgebra M α в N равны, если они совпадают на всех образах single a m.

LaTeX

$$$\forall a,m,\ f(single a m) = g(single a m)\implies f = g$$$

Lean4

theorem distribMulActionHom_ext [DistribMulAction R M] [DistribMulAction R N] {α : Type*}
    {f g : SkewMonoidAlgebra M α →+[R] N} (h : ∀ (a : α) (m : M), f (single a m) = g (single a m)) : f = g :=
  DistribMulActionHom.toAddMonoidHom_injective <| addHom_ext h

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