diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md index e40a0eefc9..0b09057a37 100644 --- a/src/elementary-number-theory/mediant-integer-fractions.lagda.md +++ b/src/elementary-number-theory/mediant-integer-fractions.lagda.md @@ -38,7 +38,7 @@ mediant-fraction-ℤ (a , b , p) (c , d , q) = ## Properties -### The mediant preserves cross-multiplication difference +### The mediant preserves the cross-multiplication difference ```agda cross-mul-diff-left-mediant-fraction-ℤ :