Commit 2025-04-25 06:33 8cb295bb

View on Github →

feat(Algebra/BigOperators/Finprod): add mul_finsum_mem / finsum_mem_mul (#24336) This PR adds the analogues of mul_finsum and finsum_mul for finsum_mem.

Estimated changes

added theorem finsum_mem_mul
added theorem mul_finsum_mem