Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 06:02 330129d4

View on Github →

feat(data/finset/lattice): inf and sup on complete_linear_orders produce an element of the set (#6103)

Estimated changes