Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes