feat(Data/List/Basic): lemma about sums of lists (leanprover-community#37407)

Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

Author: Paul-Lez

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -216,6 +216,11 @@ theorem mul_prod_eraseIdx {i} (hlen : i < l.length) (hcomm : ∀ a' ∈ l.take i
       hcomm a' (by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem)),
     insertIdx_eraseIdx_getElem hlen]
 
+@[to_additive (attr := simp)]
+theorem prod_filter_bne_one [BEq M] [LawfulBEq M] (l : List M) :
+    (l.filter (· != 1)).prod = l.prod := by
+  classical induction l <;> grind
+
 end Monoid
 
 section CommMonoid