Theorem finsum_mul'

Modification history

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