Commit 2022-01-11 13:55 eb9c1525
View on Github →feat(algebra/order/field): lemmas relating a / b
and a
when 1 ≤ b
and 1 < b
(#11333)
This PR is a collection of items that https://github.com/leanprover-community/mathlib/pull/7891 adds in and that aren't declared on master
yet. Please let me know if I overlooked something.
After merging it, https://github.com/leanprover-community/mathlib/pull/7891 can theoretically be closed.