addHom_ext — Mathlib

English

If two additive homomorphisms f,g from the direct sum agree on all injections of coordinates, then f = g.

Русский

Если два аддитивных гомоморфизма f, g из прямой суммы совпадают на всех вложениях координат, то f = g.

LaTeX

$$$\forall i,\forall y\in \β_i,\ f(\mathrm{of}\ i\ y)=g(\mathrm{of}\ i\ y)\Rightarrow f=g$$$

Lean4

/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal. -/
theorem addHom_ext {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄
    (H : ∀ (i : ι) (y : β i), f (of _ i y) = g (of _ i y)) : f = g :=
  DFinsupp.addHom_ext H

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