Extensionality principles for DFinsupp #
Main results #
DFinsupp.addHom_ext,DFinsupp.addHom_ext': if two additive homomorphisms fromΠ₀ i, β iare equal on eachsingle 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 (DFinsupp.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 (DFinsupp.single i y) = g (DFinsupp.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 (DFinsupp.singleAddHom β x) = g.comp (DFinsupp.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].