Commit 2023-11-17 13:15 ac1ea489

View on Github →

chore(Order): replace Top and Bot ancestors with OrderTop and OrderBot (#8446)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

Modified Mathlib/Order/Heyting/Basic.lean