doc(order/succ_pred/basic): fix typo (#12501)

leanprover-community · Mar 8, 2022 · 65095fe · 65095fe
1 parent 47182da
commit 65095fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/order/succ_pred/basic.lean b/src/order/succ_pred/basic.lean
@@ -23,7 +23,7 @@ order...
 * `pred_order`: Order equipped with a sensible predecessor function.
 * `is_succ_archimedean`: `succ_order` where `succ` iterated to an element gives all the greater
   ones.
-* `is_pred_archimedean`: `pred_order` where `pred` iterated to an element gives all the greater
+* `is_pred_archimedean`: `pred_order` where `pred` iterated to an element gives all the smaller
   ones.
 
 ## Implementation notes