Skip to content

Commit

Permalink
Update src/elementary-number-theory/mediant-integer-fractions.lagda.md
Browse files Browse the repository at this point in the history
Co-authored-by: Fredrik Bakke <[email protected]>
  • Loading branch information
malarbol and fredrik-bakke authored Feb 27, 2024
1 parent a576a61 commit 9e95664
Showing 1 changed file with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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-ℤ)
Expand Down

0 comments on commit 9e95664

Please sign in to comment.