doc(Algebra/Order/Group/Defs): fix typo monoid -> group for `Line…

…arOrderedAddCommGroupWithTop` (#9266)
leanprover-community · Dec 26, 2023 · cb22168 · cb22168
1 parent 6f7d92d
commit cb22168
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/Order/Group/Defs.lean b/Mathlib/Algebra/Order/Group/Defs.lean
@@ -1097,7 +1097,7 @@ addition is monotone. -/
 class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, LinearOrder α
 #align linear_ordered_add_comm_group LinearOrderedAddCommGroup
 
-/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
+/-- A linearly ordered commutative group with an additively absorbing `⊤` element.
   Instances should include number systems with an infinite element adjoined. -/
 class LinearOrderedAddCommGroupWithTop (α : Type*) extends LinearOrderedAddCommMonoidWithTop α,
   SubNegMonoid α, Nontrivial α where