Theorem mul_finsum'

Modification history

2025-10-13 13:12
Mathlib/Algebra/BigOperators/Finprod.lean
feat: commutativity of `mul` and `finprod` (#30326) …
Added mul_finsum'View on Github →