Commit 2020-08-13 07:52 c503b7af

View on Github →

feat(algebra/order): more lemmas for projection notation (#3753) Also import tactic.lint and ensure that the linter passes Move ge_of_eq to this file

Estimated changes

Modified src/algebra/order.lean

added theorem eq.trans_le

modified theorem ge_iff_le

added theorem ge_of_eq

modified theorem gt_iff_lt

added theorem has_le.le.trans_eq

modified theorem le_implies_le_of_le_of_le

added theorem le_rfl

Modified src/order/basic.lean

deleted theorem ge_of_eq

Modified src/order/filter/germ.lean