Update 0-introduction.tex

pitmonticone · Apr 15, 2024 · 279c923 · 279c923
1 parent f2012e3
commit 279c923
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/blueprint/src/chapters/0-introduction.tex b/blueprint/src/chapters/0-introduction.tex
@@ -21,7 +21,7 @@ \chapter{Introduction}
 \end{lemma}
 \begin{proof}
     \leanok
-    % TODO
+    See \href{https://pitmonticone.github.io/FLT3/docs/FLT3/Mathlib/NumberTheory/FLT/Basic.html#fermatLastTheoremWith_of_fermatLastTheoremWith_coprime}{Mathlib}.
 \end{proof}
 
 \begin{theorem}
@@ -166,7 +166,7 @@ \chapter{Introduction}
 \end{theorem}
 \begin{proof}
     \leanok
-    See \href{https://pitmonticone.github.io/FLT3/docs/FLT3/Mathlib/NumberTheory/Cyclotomic/Rat.html#IsPrimitiveRoot.zeta_sub_one_prime'}{Mathlib.NumberTheory.Cyclotomic.Rat}.
+    See \href{https://pitmonticone.github.io/FLT3/docs/FLT3/Mathlib/NumberTheory/Cyclotomic/Rat.html#IsPrimitiveRoot.zeta_sub_one_prime'}{Mathlib}.
 \end{proof}
 
 \begin{lemma}