Finitely supported functions on disjoint unions

Finsupp.sumElim_inj characterizes equality of finitely supported functions obtained by joining functions on two disjoint domains.

@[simp]

theorem Finsupp.sumElim_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] {a a' : α →₀ γ} {b b' : β →₀ γ} : a.sumElim b = a'.sumElim b' ↔ a = a' ∧ b = b'

Joining finitely supported functions on disjoint domains is injective in both arguments.