From 37e2712821bce4031e80cee9c80b26753c96dc7c Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 27 Feb 2024 18:41:28 +0100 Subject: [PATCH] Update src/elementary-number-theory/inequality-rational-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../inequality-rational-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index 5e31e673c8..74238b24f9 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -95,7 +95,7 @@ antisymmetric-leq-ℚ x y H H' = ( fraction-ℚ y) ( H) ( H'))) ∙ - ( in-fraction-fraction-ℚ y) + ( in-fraction-fraction-ℚ y) ``` ### Strict inequality on rationals is asymmetric