mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

chore: move LinearOrder Nat instance to Mathlib.Order

Open Ruben-VandeVelde opened this issue 9 months ago • 0 comments


Preliminary to removing the order dependency from Mathlib/Data/Nat/Defs.lean, but that needs a little more work

Open in Gitpod

Ruben-VandeVelde avatar May 21 '24 12:05 Ruben-VandeVelde