Commit 2025-04-06 19:50 3a141dd2

View on Github →

feat: ¬ a < b ↔ a ≤ b → b ≤ a (#23737) ... and other lemmas that are useful to link the various definitions of minimality of an element.

Estimated changes