Commit 2025-04-21 06:29 20029206
View on Github →feat: don't delaborate to ⊔ or ⊓ if we have a LinearOrder (#23558)
This PR changes the ⊔ and ⊓ notations to only be used by the delaborator if the type in question is not a linear order.
This was suggested here #mathlib4 > max and min delaborators @ 💬