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