Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-29 06:03 0de4bba3

View on Github →

feat(ordered_group): add missing instance (#1094)

Estimated changes