Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 11:59 8bc26d13

View on Github →

feat(algebra/order): ne_iff_lt_iff_le

Estimated changes

Modified src/algebra/order.lean

added theorem ne_iff_lt_iff_le

Modified src/data/buffer/parser/basic.lean

deleted theorem nat.le_of_sub_eq_pos

deleted theorem ne_iff_lt_iff_le