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

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · 39a8b54 · 39a8b54
1 parent 86e09b2
commit 39a8b54
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
@@ -76,8 +76,8 @@ cross-mul-diff-right-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
         ( mul-ℤ ny dy))
   ＝ ny *ℤ (dx +ℤ dy) -ℤ (nx +ℤ ny) *ℤ dy
     by ap-diff-ℤ
-      ( inv ( left-distributive-mul-add-ℤ ny dx dy))
-      ( inv ( right-distributive-mul-add-ℤ nx ny dy))
+      ( inv (left-distributive-mul-add-ℤ ny dx dy))
+      ( inv (right-distributive-mul-add-ℤ nx ny dy))
 ```
 
 ## External links