Theorem mul_finsum_mem'

Modification history

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