Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-26 18:55 26dfea59

View on Github →

feat(algebra/big_operators): sum of two products (#3944)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.mul_prod_diff_singleton

added theorem finset.prod_add_prod_eq

added theorem finset.prod_inter_mul_prod_diff

Modified src/algebra/big_operators/order.lean

added theorem finset.prod_add_prod_le'

added theorem finset.prod_add_prod_le

Modified src/algebra/group_with_zero_power.lean

added theorem zero_pow_eq_zero

Modified src/algebra/ordered_ring.lean

added theorem canonically_ordered_semiring.mul_le_mul_left'

added theorem canonically_ordered_semiring.mul_le_mul_right'