feat(finsupp/basic): add hom_ext (#3941)
feat(finsupp/basic): add hom_ext (#3941)

Two R-module homs from finsupp X R which agree on `single x 1` agree everywhere.
```
lemma hom_ext [semiring β] [add_comm_monoid γ] [semimodule β γ] (φ ψ : (α →₀ β) →ₗ[β] γ)
  (h : ∀ a : α, φ (single a 1) = ψ (single a 1)) : φ = ψ
```





leanprover-community/mathlib,leanprover-community/mathlib