Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-28 11:17 fa230957

View on Github →

fix(algebra/big_operators): add missing to_additives (#18878) These lemmas were written before pi.mul_single existed.

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.prod_erase_lt_of_one_lt

added theorem finset.prod_pi_mul_single'

added theorem finset.prod_pi_mul_single

deleted theorem finset.sum_erase_lt_of_pos

deleted theorem finset.sum_pi_single'

deleted theorem finset.sum_pi_single

Modified src/algebra/big_operators/pi.lean

deleted theorem add_monoid_hom.functions_ext'

deleted theorem add_monoid_hom.functions_ext

added theorem finset.univ_prod_mul_single

deleted theorem finset.univ_sum_single

added theorem monoid_hom.functions_ext'

added theorem monoid_hom.functions_ext