forgot to run precommit before committing

UniMath · Dec 22, 2024 · 11277a3 · 11277a3
1 parent eda22b0
commit 11277a3
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
@@ -48,6 +48,7 @@ open import elementary-number-theory.divisibility-natural-numbers public
 open import elementary-number-theory.divisibility-standard-finite-types public
 open import elementary-number-theory.equality-integers public
 open import elementary-number-theory.equality-natural-numbers public
+open import elementary-number-theory.equality-rational-numbers public
 open import elementary-number-theory.euclid-mullin-sequence public
 open import elementary-number-theory.euclidean-division-natural-numbers public
 open import elementary-number-theory.eulers-totient-function public

diff --git a/src/elementary-number-theory/equality-rational-numbers.lagda.md b/src/elementary-number-theory/equality-rational-numbers.lagda.md
@@ -12,7 +12,6 @@ open import elementary-number-theory.rational-numbers
 
 open import foundation.identity-types
 open import foundation.universe-levels
-
 ```
 
 </details>
@@ -37,9 +36,9 @@ Eq-eq-ℚ {x} {.x} refl = refl-Eq-ℚ x
 
 eq-Eq-ℚ : (x y : ℚ) → Eq-ℚ x y → x ＝ y
 eq-Eq-ℚ x y H = equational-reasoning
-  x ＝ rational-fraction-ℤ (fraction-ℚ x) by inv (is-retraction-rational-fraction-ℚ x)
-  ＝ rational-fraction-ℤ (fraction-ℚ y)  by eq-ℚ-sim-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H
+  x ＝ rational-fraction-ℤ (fraction-ℚ x)
+    by inv (is-retraction-rational-fraction-ℚ x)
+  ＝ rational-fraction-ℤ (fraction-ℚ y)
+    by eq-ℚ-sim-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H
   ＝ y by is-retraction-rational-fraction-ℚ y
-
-
 ```