Update 2-case2.tex

blueprint/src/chapters/2-case2.tex

@@ -6,7 +6,6 @@ \chapter*{Case 2}
     \label{lmm:three_dvd_gcd_of_dvd_a_of_dvd_b}
     \lean{three_dvd_gcd_of_dvd_a_of_dvd_b}
     \leanok
-    %\uses{}
     Let $a, b, c \in \N$. \\
     Let $3 \divides a$ and $3 \divides b$. \\
     Let $a ^ 3 + b ^ 3 = c ^ 3$. \\\\
@@ -34,9 +33,10 @@ \chapter*{Case 2}
     \label{lmm:three_dvd_gcd_of_dvd_b_of_dvd_c}
     \lean{three_dvd_gcd_of_dvd_b_of_dvd_c}
     \leanok
-    %\uses{}
     Let $a, b, c \in \N$. \\
-    If $3 \divides b$ and $3 \divides c$ and $a ^ 3 + b ^ 3 = c ^ 3$, then $3 \divides \gcd(\set{a, b, c})$.
+    Let $3 \divides b$ and $3 \divides c$. \\
+    Let $a ^ 3 + b ^ 3 = c ^ 3$. \\\\
+    Then $3 \divides \gcd(\set{a, b, c})$.
 \end{lemma}
 \begin{proof}
     \leanok
@@ -63,16 +63,20 @@ \chapter*{Case 2}
     }
 \end{proof}
 
+Let $K$ be a number field (cyclotomic extension $\Q[e^{\frac{2\pi i}{3}}]$). \\
+Let $\cc{O}_K$ be the ring of integers of $K$. \\
+Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+Let $\zeta \in K$ be any primitive $3$-rd root of unity. \\
+Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta \in K$. \\
+Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
+Let $u \in \cc{O}^\times_K$.
+
 \begin{definition}[Solution']
     \label{def:Solution1}
     \lean{Solution'}
     \leanok
-    Let $K$ be a number field. \\
-    Let $\cc{O}_K$ be the ring of integers of $K$. \\
-    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
-    Let $a, b, c \in \cc{O}_K$ such that $\lambda \notdivides a$,
-    $\lambda \notdivides b$, $\lambda \divides c$, $c \neq 0$ and $\gcd(a,b)=1$.\\
-    Let $u \in \cc{O}^\times_K$. \\\\
+    Let $a, b, c \in \cc{O}_K$ such that $c \neq 0$ and $\gcd(a,b)=1$.\\
+    Let $\lambda \notdivides a$, $\lambda \notdivides b$ and $\lambda \divides c$. \\\\
     A $\boldsymbol{solution'}$ is a tuple $(a, b, c, u)$
     satisfying the equation $a^3 + b^3 = u \cdot c^3.$
 \end{definition}
@@ -81,15 +85,11 @@ \chapter*{Case 2}
     \label{def:Solution}
     \lean{Solution}
     \leanok
-    Let $K$ be a number field. \\
-    Let $\cc{O}_K$ be the ring of integers of $K$. \\
-    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
-    Let $a, b, c \in \cc{O}_K$ such that $\lambda \notdivides a$,
-    $\lambda \notdivides b$, $\lambda \divides c$, $c \neq 0$, $\gcd(a,b)=1$
-    and $\lambda^2 \divides a+b$. \\
-    Let $u \in \cc{O}^\times_K$. \\\\
+    Let $a, b, c \in \cc{O}_K$ such that $c \neq 0$ and $\gcd(a,b)=1$.\\
+    Let $\lambda \notdivides a$, $\lambda \notdivides b$, $\lambda \divides c$ and
+    $\lambda^2 \divides a+b$. \\\\
     A $\boldsymbol{solution}$ is a tuple $(a, b, c, u)$
-    satisfying the equation $a^3 + b^3 = u \cdot c^3.$
+    satisfying the equation $a^3 + b^3 = u \cdot c^3$.
 \end{definition}
 
 \begin{lemma}
@@ -693,7 +693,7 @@ \chapter*{Case 2}
     Let $\cc{O}_K$ be the ring of integers of $K$. \\
     Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
     Let $a, b, c \in \cc{O}_K$ such that $c \neq 0$ and $\gcd(a,b)=1$. \\
-    Let $u \in \cc{O}^\times_K$ \\
+    Let $u \in \cc{O}^\times_K$. \\
     Let $\lambda \notdivides a$, $\lambda \notdivides b$ and $\lambda \divides c$. \\\\
     Then $a^3 + b^3 \neq u \cdot c^3$.
 \end{theorem}