Commit 2023-07-01 11:38 2fd9a721

feat(Algebra/BigOperators/Finprod): variations on smul_finsum (#5601) The current versions of smul_finsum and finsum_smul assume NoZeroSMulDivisors in order to be a little bit clever about the junk values (that's why there's no finite support hypothesis). While this is reasonable in a lot of cases, there are also cases where we already know that the sum is well-defined, so we don't need this extra assumption.