Commit 2025-10-13 13:12 5b27418a

View on Github →

feat: commutativity of mul and finprod (#30326) For (semi-)rings without zero divisors, show that multiplication commutes with finprod. Following a brief discussion of Zulip, unify naming between theorems about multiplication and theorems about scalar multiplication.

Estimated changes

added theorem finsum_mem_mul'
modified theorem finsum_mem_mul
added theorem finsum_mul'
modified theorem finsum_mul
added theorem mul_finsum'
modified theorem mul_finsum
added theorem mul_finsum_mem'
modified theorem mul_finsum_mem