mathlib
9db43a5f
- chore(data/nat/basic): remove pos_iff_ne_zero' (#1610)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
chore(data/nat/basic): remove pos_iff_ne_zero' (#1610) This used to be different from pos_iff_ne_zero because the latter was phrased in terms of `n > 0`, not `0 < n`. Since #1436 they are the same.
References
#1610 - chore(data/nat/basic): remove pos_iff_ne_zero'
Author
rwbarton
Committer
mergify[bot]
Parents
151bcbe2
Loading