Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 11:49 d94772bb

View on Github →

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

Estimated changes

Modified src/algebra/big_operators/finprod.lean

added theorem finprod_div_distrib

added theorem finprod_mem_div_distrib

added theorem finprod_mem_inv_distrib

added theorem mul_equiv.map_finprod_mem