Theorems · Theorem · general algebraic systems

DFinsupp.addHom_ext

∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
  [inst_2 : AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄,
  (∀ (i : ι) (y : β i), (f fun₀ | i => y) = g fun₀ | i => y) → f = g

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

Defined in

Mathlib.Data.DFinsupp.Ext

Cited by

4 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddZeroClassAddZeroClass