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.