Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-06 08:01 d1ae307b

View on Github →

chore(algebra/ordered_group): add exists_pos_add_of_lt (#2967) Also drop protected on _root_.zero_lt_iff_ne_zero.

Estimated changes

added theorem exists_pos_add_of_lt
added theorem zero_lt_iff_ne_zero