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.

@[simp]

theorem DFinsupp.add_closure_iUnion_range_single {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] : AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) = ⊤

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.

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].

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)