Mathlib v3 is deprecated. Go to Mathlib v4

Theorem abs_nonneg'

Modification history

2021-03-24 16:04
test/linarith.lean
feat(tactic/lint): linter for @[class] def (#6061) …
Modified abs_nonneg'View on Github →
2020-09-03 00:15
test/linarith.lean
fix(test/*): make sure tests produce no output (#3947) …
Modified abs_nonneg'View on Github →
2020-07-17 09:26
test/linarith.lean
fix(tactic/nlinarith): stop nlinarith failing in the presence of squares when there is no order (#3417) …
Added abs_nonneg'View on Github →