Commit 2025-07-27 10:52 3e7682ba
View on Github →feat(AlgebraicGeometry): Add global preorder instance for schemes (#26204) In this PR we added a default preorder instance for schemes, defined to be the specialization order as discussed here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/dimension.20function.20for.20schemes/near/524997376 for discussion