Update src/elementary-number-theory/mediant-integer-fractions.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · a576a61 · a576a61
1 parent 37e2712
commit a576a61
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md
@@ -63,8 +63,8 @@ cross-mul-diff-left-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
 cross-mul-diff-right-mediant-fraction-ℤ :
   (x y : fraction-ℤ) →
   Id
-    (cross-mul-diff-fraction-ℤ x y)
-    (cross-mul-diff-fraction-ℤ (mediant-fraction-ℤ x y) y)
+    ( cross-mul-diff-fraction-ℤ x y)
+    ( cross-mul-diff-fraction-ℤ (mediant-fraction-ℤ x y) y)
 cross-mul-diff-right-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
   equational-reasoning
   (ny *ℤ dx -ℤ nx *ℤ dy)