Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_equiv.map_finprod_mem

Modification history

2021-11-23 11:49

src/algebra/big_operators/finprod.lean

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

Added mul_equiv.map_finprod_mem View on Github →