Mathlib v3 is deprecated. Go to Mathlib v4

Theorem neg_one_lt_zero

Modification history

2021-01-15 05:41
src/algebra/ordered_ring.lean
chore(algebra/ordered_ring): add a few simp lemmas (#5749) …
Modified neg_one_lt_zeroView on Github →
2020-06-08 15:06
src/algebra/ordered_ring.lean
chore(algebra/ordered_ring): use le instead of ge (#2986)
Added neg_one_lt_zeroView on Github →