Theorem finsum_mem_mul

Modification history

2025-10-13 13:12
Mathlib/Algebra/BigOperators/Finprod.lean
feat: commutativity of `mul` and `finprod` (#30326) …
Modified finsum_mem_mulView 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 finsum_mem_mulView on Github →