From d5fdbd6cecad001eaa1a9000aa89f0b24aae2ad8 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Apr 2024 08:55:28 +0200
Subject: [PATCH] Update 0-introduction.tex

---
 blueprint/src/chapters/0-introduction.tex | 40 ++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/blueprint/src/chapters/0-introduction.tex b/blueprint/src/chapters/0-introduction.tex
index 5983ee7..95cd32d 100644
--- a/blueprint/src/chapters/0-introduction.tex
+++ b/blueprint/src/chapters/0-introduction.tex
@@ -241,5 +241,43 @@ \chapter*{Introduction}
 \end{lemma}
 \begin{proof}
     \leanok
-    \uses{lmm:toInteger_cube_eq_one, lmm:toInteger_eval_cyclo}
+    \uses{lmm:dvd_or_dvd_sub_one_or_dvd_add_one, lmm:lambda_dvd_three}
+\end{proof}
+
+\begin{lemma}
+    \label{lmm:lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one}
+    \lean{IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one}
+    \leanok
+    %\uses{}
+    % TODO
+\end{lemma}
+\begin{proof}
+    \leanok
+    \uses{lmm:cube_sub_one, lmm:lambda_dvd_mul_sub_one_mul_sub_eta_add_one}
+\end{proof}
+
+\begin{lemma}
+    \label{lmm:lambda_pow_four_dvd_cube_add_one_of_dvd_add_one}
+    \lean{IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one}
+    \leanok
+    %\uses{}
+    % TODO
+\end{lemma}
+\begin{proof}
+    \leanok
+    \uses{lmm:lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one}
+\end{proof}
+
+\begin{lemma}
+    \label{lmm:lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd}
+    \lean{IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd}
+    \leanok
+    %\uses{}
+    % TODO
+\end{lemma}
+\begin{proof}
+    \leanok
+    \uses{lmm:dvd_or_dvd_sub_one_or_dvd_add_one,
+    lmm:lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one,
+    lmm:lambda_pow_four_dvd_cube_add_one_of_dvd_add_one}
 \end{proof}
\ No newline at end of file