Mathlib v3 is deprecated. Go to Mathlib v4

Theorem neg_neg_iff_pos

Modification history

2020-06-09 17:36
src/algebra/ordered_group.lean
refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844) …
Deleted neg_neg_iff_posView on Github →
2020-04-11 04:27
src/algebra/ordered_group.lean
chore(*): switch to lean 3.8.0 (#2361) …
Modified neg_neg_iff_posView on Github →
2019-05-29 06:03
src/algebra/ordered_group.lean
feat(ordered_group): add missing instance (#1094)
Modified neg_neg_iff_posView on Github →
2019-05-07 19:03
src/algebra/ordered_group.lean
building the hyperreal library (#835) …
Added neg_neg_iff_posView on Github →