# Extensionality principles for `DFinsupp` #

## Main results #

- `DFinsupp.addHom_ext`, `DFinsupp.addHom_ext'`: if two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then they are equal.

source
@[simp]
theorem DFinsupp.add_closure_iUnion_range_single {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] :
AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) = ⊤
source
theorem DFinsupp.addHom_ext {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) :
f = g

If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then they are equal.

source
theorem DFinsupp.addHom_ext' {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄ (H : ∀ (x : ι), f.comp (singleAddHom β x) = g.comp (singleAddHom β x)) :
f = g

If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then they are equal.

See note [partially-applied ext lemmas].

source
theorem DFinsupp.addHom_ext'_iff {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [AddZeroClass γ] {f g : (Π₀ (i : ι), β i) →+ γ} :
f = g ↔ ∀ (x : ι), f.comp (singleAddHom β x) = g.comp (singleAddHom β x)