Commit 2023-01-03 18:09 8044f03d

feat port: Order.Extension.Linear (#1309) Line 59. I needed to add an explicit haveI : IsPartialOrder α s := hs₁ otherwise the necessary instances would be missing later on (the mathlib3 file has a resetI to do this). I am not sure if it is the right way to fix that...