distribMulActionHom_ext — Mathlib

English

Two DistribMulActionHom maps are equal if they agree on all single-a inputs; i.e., equality is determined by their action on basis elements.

Русский

Два отображения DistribMulActionHom равны, если они совпадают на всех входах типа single(a,m).

LaTeX

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

Lean4

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

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