diff --git a/Mathlib/Algebra/Order/Nonneg/Field.lean b/Mathlib/Algebra/Order/Nonneg/Field.lean index 49c06d2e70cdd..0513107a568ff 100644 --- a/Mathlib/Algebra/Order/Nonneg/Field.lean +++ b/Mathlib/Algebra/Order/Nonneg/Field.lean @@ -103,6 +103,6 @@ end LinearOrderedSemifield instance linearOrderedCommGroupWithZero [LinearOrderedField α] : LinearOrderedCommGroupWithZero { x : α // 0 ≤ x } := - LinearOrderedSemifield.toLinearOrderedCommGroupWithZero + inferInstance end Nonneg