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)) : φ = ψ
```
