English
If for all x, f ∘ (singleAddHom β x) = g ∘ (singleAddHom β x), then f = g.
Русский
Если для каждого x выполняется f ∘ (singleAddHom β x) = g ∘ (singleAddHom β x), то f = g.
LaTeX
$$$\\forall x, f \\circ (\\mathrm{singleAddHom}\\, \\beta\\, x) = g \\circ (\\mathrm{singleAddHom}\\, \\beta\\, x) \\Rightarrow f = g$$$
Lean4
/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal.
See note [partially-applied ext lemmas]. -/
@[ext]
theorem addHom_ext' {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
(H : ∀ x, f.comp (singleAddHom β x) = g.comp (singleAddHom β x)) : f = g :=
addHom_ext fun x => DFunLike.congr_fun (H x)
