Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-11-09 12:33
04dd1327
View on Github →
feat(algebra/big_operators): exists_ne_(one|zero)
of
(prod|sum)
ne
(one|zero)
Estimated changes
Modified
algebra/big_operators.lean
added
theorem
finset.exists_ne_one_of_prod_ne_one