Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 07:31 e5acda42

View on Github →

chore(order/conditionally_complete_lattice): drop an unneeded nonempty assumption (#10132)

Estimated changes