Theorem mul_finsum_mem

Modification history

2025-10-13 13:12
Mathlib/Algebra/BigOperators/Finprod.lean
feat: commutativity of `mul` and `finprod` (#30326) …
Modified mul_finsum_memView on Github →
2025-04-25 06:33
Mathlib/Algebra/BigOperators/Finprod.lean
feat(Algebra/BigOperators/Finprod): add `mul_finsum_mem` / `finsum_mem_mul` (#24336) …
Added mul_finsum_memView on Github →