∀ {R : Type u_2} {S : Type u_3} (M : Type u_1) [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (v₁ v₂ : M →₀ R),
  Finsupp.mapRange ⇑f ⋯ (v₁ + v₂) = Finsupp.mapRange ⇑f ⋯ v₁ + Finsupp.mapRange ⇑f ⋯ v₂