addHom_ext' — Mathlib

English

If two additive homomorphisms f,g satisfy ∀ i, f.comp (of i) = g.comp (of i), then f = g.

Русский

Если два аддитивных гомоморфизма f,g удовлетворяют ∀ i, f∘of i = g∘of i, то f = g.

LaTeX

$$For all f,g : (⊕ i, β i) →+ γ, (∀ i, f ∘ (of β i) = g ∘ (of β i)) → f = g$$

Lean4

/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem addHom_ext' {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄
    (H : ∀ i : ι, f.comp (of _ i) = g.comp (of _ i)) : f = g :=
  addHom_ext fun i => DFunLike.congr_fun <| H i

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