Commit 2020-08-26 10:32 dd742dc8

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