Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
FR-vdash-bot committed Jan 6, 2025
1 parent de602a1 commit b05ca39
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Order/Nonneg/Field.lean
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,6 @@ end LinearOrderedSemifield

instance linearOrderedCommGroupWithZero [LinearOrderedField α] :
LinearOrderedCommGroupWithZero { x : α // 0 ≤ x } :=
LinearOrderedSemifield.toLinearOrderedCommGroupWithZero
CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero

end Nonneg

0 comments on commit b05ca39

Please sign in to comment.