mathlib

d94772bb - feat(algebra/big_operators/finprod): add finprod_div_distrib and finsum_sub_distrib (#10044)