Commit 2026-01-08 19:45 7a63161f

View on Github →

feat: some lemmas about finsum/finprod (#33186) From sphere-eversion.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

added theorem finite_mulSupport_of_finprod_ne_one

added theorem finite_support_of_finsum_eq_one

added theorem finprod_eq_prod_of_mulSupport_subset_of_finite

added theorem finprod_prod_filter

added theorem map_finprod

Modified Mathlib/Algebra/Notation/Support.lean

added theorem Subsingleton.mulSupport_eq