Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 06:34 05c491cd

View on Github →

feat(big_operators): single out one term from prod (#7040)

Estimated changes

Modified src/algebra/big_operators/basic.lean

deleted theorem finset.mul_prod_diff_singleton

added theorem finset.prod_eq_mul_prod_diff_singleton

added theorem finset.prod_eq_prod_diff_singleton_mul

modified theorem finset.prod_insert

added theorem fintype.prod_eq_mul_prod_compl

added theorem fintype.prod_eq_prod_compl_mul

Modified src/algebra/big_operators/order.lean

Modified src/number_theory/bernoulli.lean