Commit 2025-04-13 21:24 699b96b6
View on Github →chore(Surreal): dedup instance (#23985)
Deduplicates the instance LinearOrder Surreal, which was defined in both Surreal/Basic and Surreal/Multiplication.
The duplicate originated in #14044.
The surviving instance is at
https://github.com/leanprover-community/mathlib4/blob/461b2e79dd4c923f26e435f770faeaf87208d0d9/Mathlib/SetTheory/Surreal/Basic.lean#L368-L373