Mathlib Changelog
v3
Changelog
About
Github
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
Modified
algebra/big_operators.lean
added
theorem
exists_false
added
theorem
finset.mul_sum
added
theorem
finset.prod_const_one
added
theorem
finset.prod_eq_zero
added
theorem
finset.prod_eq_zero_iff
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