From 8362b812ee6c5ae0ec90a3b869734b425084745b Mon Sep 17 00:00:00 2001
From: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Date: Mon, 11 Aug 2025 14:21:47 +0000
Subject: [PATCH] typos

---
 blueprint/src/rationals.tex | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/blueprint/src/rationals.tex b/blueprint/src/rationals.tex
index 97796b0..dd7f2f0 100644
--- a/blueprint/src/rationals.tex
+++ b/blueprint/src/rationals.tex
@@ -36,7 +36,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
     \leanok
     \uses{MyPrerat.R}
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -48,7 +48,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
     \leanok
     \uses{MyPrerat.R}
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -60,7 +60,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
     \leanok
     \uses{MyPrerat.R}
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -98,7 +98,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
 \uses{MyPrerat.neg}
 \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{definition}
@@ -107,7 +107,7 @@ \section{The \emph{prerationals}}
     \leanok
     \uses{MyPrerat.R}
 We define an operation, called \emph{addition} on $\MyPrerat$ as follows: the addition of $x = (a,b)$
-and $y = (b, c)$ is
+and $y = (c, d)$ is
 \[
 x + y = (a,b) + (c,d) = (a * d + b * c, b*d)
 \]
@@ -123,7 +123,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
 \uses{MyPrerat.add}
 \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{definition}
@@ -146,7 +146,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
 \uses{MyPrerat.mul}
 \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{definition}
@@ -170,7 +170,7 @@ \section{The \emph{prerationals}}
 \begin{proof}
 \uses{MyPrerat.inv}
 \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \section{The rationals}
@@ -449,7 +449,7 @@ \subsection{\texorpdfstring{The inclusion $j \colon \MyInt \to \MyRat$}{The incl
 \begin{proof}
     \uses{MyRat.add, MyRat.j}
     \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -464,7 +464,7 @@ \subsection{\texorpdfstring{The inclusion $j \colon \MyInt \to \MyRat$}{The incl
 \begin{proof}
     \uses{MyRat.mul, MyRat.j}
     \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -476,7 +476,7 @@ \subsection{\texorpdfstring{The inclusion $j \colon \MyInt \to \MyRat$}{The incl
 \begin{proof}
     \uses{MyRat.j}
     \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -500,7 +500,7 @@ \subsection{\texorpdfstring{The inclusion $j \colon \MyInt \to \MyRat$}{The incl
 \begin{proof}
     \uses{MyRat.inv, MyRat.mul, MyRat.j}
     \leanok
-Exercice.
+Exercise.
 \end{proof}
 
 \subsection{Nonegativity}
@@ -562,7 +562,7 @@ \subsection{Nonegativity}
 \end{lemma}
 \begin{proof}
     \leanok
-    Annoying but easy, left as an exercice.
+    Annoying but easy, left as an exercise.
 \end{proof}
 
 \begin{lemma}
@@ -574,7 +574,7 @@ \subsection{Nonegativity}
 \end{lemma}
 \begin{proof}
     \leanok
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -586,7 +586,7 @@ \subsection{Nonegativity}
 \end{lemma}
 \begin{proof}
     \leanok
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -598,7 +598,7 @@ \subsection{Nonegativity}
 \end{lemma}
 \begin{proof}
     \leanok
-    Exercice.
+    Exercise.
 \end{proof}
 
 \subsection{The order}
@@ -713,7 +713,7 @@ \subsection{Interaction between the order and the inclusions}
 \begin{proof}
     \uses{MyRat.IsNonneg, MyInt.le}
     \leanok
-    Exercice.
+    Exercise.
 \end{proof}
 
 \begin{lemma}
@@ -763,7 +763,7 @@ \subsection{The linear order structure}
 \begin{proof}
     \leanok
     \uses{MyRat.zero_le_iff_IsNonneg, MyRat.isNonneg_mul_isNonneg}
-Exercice.
+Exercise.
 \end{proof}
 
 We now have that $\MyRat$ is a \emph{strict ordered ring}: a nontrivial ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.
\ No newline at end of file