refactor(Order/Extension): use OrderHom (#9232)

Redefine `toLinearExtension` as an `OrderHom`.
leanprover-community · Dec 23, 2023 · bb307ab · bb307ab
1 parent 539b49a
commit bb307ab
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/Mathlib/Order/Extension/Linear.lean b/Mathlib/Order/Extension/Linear.lean
@@ -86,12 +86,10 @@ noncomputable instance {α : Type u} [PartialOrder α] : LinearOrder (LinearExte
   le_total := (extend_partialOrder ((· ≤ ·) : α → α → Prop)).choose_spec.choose.2.1
   decidableLE := Classical.decRel _
 
-/-- The embedding of `α` into `LinearExtension α` as a relation homomorphism. -/
-def toLinearExtension {α : Type u} [PartialOrder α] :
-    ((· ≤ ·) : α → α → Prop) →r ((· ≤ ·) : LinearExtension α → LinearExtension α → Prop)
-    where
+/-- The embedding of `α` into `LinearExtension α` as an order homomorphism. -/
+def toLinearExtension {α : Type u} [PartialOrder α] : α →o LinearExtension α where
   toFun x := x
-  map_rel' := (extend_partialOrder ((· ≤ ·) : α → α → Prop)).choose_spec.choose_spec _ _
+  monotone' := (extend_partialOrder ((· ≤ ·) : α → α → Prop)).choose_spec.choose_spec
 #align to_linear_extension toLinearExtension
 
 instance {α : Type u} [Inhabited α] : Inhabited (LinearExtension α) :=