From 9e9566458cfc7a0ddefd707974ae74592df961fa Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 27 Feb 2024 19:03:57 +0100 Subject: [PATCH] Update src/elementary-number-theory/mediant-integer-fractions.lagda.md Co-authored-by: Fredrik Bakke --- .../mediant-integer-fractions.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md index 40e7ef0fd6..460a12d961 100644 --- a/src/elementary-number-theory/mediant-integer-fractions.lagda.md +++ b/src/elementary-number-theory/mediant-integer-fractions.lagda.md @@ -57,8 +57,8 @@ cross-mul-diff-left-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) = ( mul-ℤ nx dx)) ＝ (nx +ℤ ny) *ℤ dx -ℤ nx *ℤ (dx +ℤ dy) by ap-diff-ℤ - ( inv ( right-distributive-mul-add-ℤ nx ny dx)) - ( inv ( left-distributive-mul-add-ℤ nx dx dy)) + ( inv (right-distributive-mul-add-ℤ nx ny dx)) + ( inv (left-distributive-mul-add-ℤ nx dx dy)) cross-mul-diff-right-mediant-fraction-ℤ : (x y : fraction-ℤ) →