fix

leanprover-community · Jan 6, 2025 · de602a1 · de602a1
1 parent dbcd3d4
commit de602a1
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Algebra/Order/Field/Canonical.lean b/Mathlib/Algebra/Order/Field/Canonical.lean
@@ -19,6 +19,7 @@ variable {α : Type*} [Semifield α] [LinearOrder α] [CanonicallyOrderedAdd α]
 abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero α :=
   { __ := ‹Semifield α›
+    __ := ‹LinearOrder α›
     zero_le_one := zero_le_one
     mul_le_mul_left := fun _ _ h _ ↦ mul_le_mul_of_nonneg_left h <| zero_le _ }