Commit 2023-05-08 00:54 828c8139

View on Github →

chore: forward-port leanprover-community/mathlib#18878 (#3742)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_erase_lt_of_one_lt

added theorem Finset.prod_pi_mulSingle'

added theorem Finset.prod_pi_mulSingle

deleted theorem Finset.sum_erase_lt_of_pos

deleted theorem Finset.sum_pi_single'

deleted theorem Finset.sum_pi_single

Modified Mathlib/Algebra/BigOperators/Pi.lean

deleted theorem AddMonoidHom.functions_ext'

deleted theorem AddMonoidHom.functions_ext

added theorem Finset.univ_prod_mulSingle

deleted theorem Finset.univ_sum_single

added theorem MonoidHom.functions_ext'

added theorem MonoidHom.functions_ext