mathlib
c503b7af - feat(algebra/order): more lemmas for projection notation (#3753)

Commit

5 years ago

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

Author

fpvandoorn

Parents

6c8b2cd6

mathlib c503b7af - feat(algebra/order): more lemmas for projection notation (#3753)

mathlib
c503b7af - feat(algebra/order): more lemmas for projection notation (#3753)