Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_abs_nonneg

Modification history

2022-11-06 23:41
src/algebra/order/group/abs.lean
refactor(*): supremum of several recent refactoring PRs (#17381) …
Modified add_abs_nonnegView on Github →
2022-06-01 13:00
src/algebra/order/group.lean
feat(algebra/order/group): helper lemma `0 ≤ a + |a|` (#14457) …
Added add_abs_nonnegView on Github →