Mathlib v3 is deprecated. Go to Mathlib v4

Theorem T.zero_lt_one

Modification history

2021-03-24 16:04
test/linarith.lean
feat(tactic/lint): linter for @[class] def (#6061) …
Modified T.zero_lt_oneView on Github →
2020-09-03 00:15
test/linarith.lean
fix(test/*): make sure tests produce no output (#3947) …
Modified T.zero_lt_oneView on Github →
2020-07-19 15:29
test/linarith.lean
fix(tactic/linarith): find correct zero_lt_one (#3455) …
Added T.zero_lt_oneView on Github →