Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-28 21:30 edfbf3cf

View on Github →

feat(algebra/big_operators): add semiring and integral_domain rules

Estimated changes

added theorem exists_false
added theorem finset.mul_sum
added theorem finset.prod_const_one
added theorem finset.prod_eq_zero
modified theorem finset.prod_hom
modified theorem finset.prod_inv_distrib
added theorem finset.sum_le_sum
added theorem finset.sum_le_zero
added theorem finset.sum_mul
modified theorem finset.sum_sub_distrib
added theorem finset.zero_le_sum