feat(Finsupp): single a (m₁ + m₂) b = single a m₁ b + single a m₂ b (leanprover-community#27191)

From Toric

Author: YaelDillies

Mathlib/Data/Finsupp/Single.lean

@@ -521,6 +521,9 @@ variable [AddZeroClass M]
 theorem single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
   (zipWith_single_single _ _ _ _ _).symm
 
+lemma single_add_apply (a : α) (m₁ m₂ : M) (b : α) :
+    single a (m₁ + m₂) b = single a m₁ b + single a m₂ b := by simp
+
 theorem support_single_add {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
     support (single a b + f) = cons a f.support ha := by
   classical