From 5a9a306b1871c11c46e2a53fd2a3aef86c5ee348 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 16:27:14 +0200 Subject: [PATCH 1/7] Add python virtual environment to .gitignore --- .gitignore | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 2bc8af4f..a5ddc900 100644 --- a/.gitignore +++ b/.gitignore @@ -15,4 +15,5 @@ blueprint/lean_decls *.log *.out *.pdf - +# Python virtual environment +/.venv \ No newline at end of file From f7a5614e4c5b4aea486bb597a70ad5b5f406bf37 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:14:05 +0200 Subject: [PATCH 2/7] Update .gitignore --- .gitignore | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 82c66318..db8a47ff 100644 --- a/.gitignore +++ b/.gitignore @@ -6,8 +6,11 @@ # Lean blueprint blueprint/print/print.log blueprint/web/ +blueprint/src/web.paux +blueprint/src/web.bbl blueprint/print/ -blueprint/lean_decls # KB guesses this is safe (he's asked Patrick) +# KB guesses this is safe (he's asked Patrick) +blueprint/lean_decls # Files generated by LaTeX *.aux *.bbl From caf3ffb0f367224820e4fc93361a8d2af31fcdb5 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:25:48 +0200 Subject: [PATCH 3/7] Fix bibliography warnings in web.tex --- blueprint/src/web.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index cbbd159f..bb09d84f 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -18,6 +18,10 @@ \github{https://github.com/ImperialCollegeLondon/FLT/} \dochome{https://ImperialCollegeLondon.github.io/FLT/docs} +\usepackage[style=trad-alpha]{biblatex} +\ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} +\bibliography{bibliography.bib} + \title{A Blueprint for Fermat's Last Theorem} \author{Kevin Buzzard, Richard Taylor} From 4d58c5a8629df1812cad45f0095930b3d5382f4c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:25:54 +0200 Subject: [PATCH 4/7] Fix bibliography warnings in print.tex --- blueprint/src/print.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 00afcb23..8f0fe0cc 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -34,6 +34,10 @@ \title{A Lean proof of Fermat's Last Theorem} \author{Kevin Buzzard, Richard Taylor} +\usepackage[style=trad-alpha]{biblatex} +\ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} +\bibliography{bibliography.bib} + \begin{document} \maketitle \input{content} From eb94a8eb4480e14084cefeb0cf3831afc462d66a Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:28:32 +0200 Subject: [PATCH 5/7] Fix path --- blueprint/src/print.tex | 2 +- blueprint/src/web.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 8f0fe0cc..5d660ef7 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -36,7 +36,7 @@ \usepackage[style=trad-alpha]{biblatex} \ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} -\bibliography{bibliography.bib} +\bibliography{biblio.bib} \begin{document} \maketitle diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index bb09d84f..efb51fd4 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -20,7 +20,7 @@ \usepackage[style=trad-alpha]{biblatex} \ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} -\bibliography{bibliography.bib} +\bibliography{biblio.bib} \title{A Blueprint for Fermat's Last Theorem} \author{Kevin Buzzard, Richard Taylor} From bf6fd5a09b11dfcd33890dbbf886f0a789eaa871 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:37:35 +0200 Subject: [PATCH 6/7] Revert biblio changes --- blueprint/src/print.tex | 4 ---- blueprint/src/web.tex | 4 ---- 2 files changed, 8 deletions(-) diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 5d660ef7..00afcb23 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -34,10 +34,6 @@ \title{A Lean proof of Fermat's Last Theorem} \author{Kevin Buzzard, Richard Taylor} -\usepackage[style=trad-alpha]{biblatex} -\ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} -\bibliography{biblio.bib} - \begin{document} \maketitle \input{content} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index efb51fd4..cbbd159f 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -18,10 +18,6 @@ \github{https://github.com/ImperialCollegeLondon/FLT/} \dochome{https://ImperialCollegeLondon.github.io/FLT/docs} -\usepackage[style=trad-alpha]{biblatex} -\ExecuteBibliographyOptions{safeinputenc=true,backref=true,giveninits,useprefix=true,maxnames=5,doi=false,eprint=true,isbn=false,url=false} -\bibliography{biblio.bib} - \title{A Blueprint for Fermat's Last Theorem} \author{Kevin Buzzard, Richard Taylor} From 085d513fa1ffb997f77d386fdc83bc8b0d34aacf Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 1 May 2024 17:59:50 +0200 Subject: [PATCH 7/7] Fix label bug --- blueprint/src/chapter/ch03frey.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/chapter/ch03frey.tex b/blueprint/src/chapter/ch03frey.tex index 44b76a69..6aa0a58b 100644 --- a/blueprint/src/chapter/ch03frey.tex +++ b/blueprint/src/chapter/ch03frey.tex @@ -410,6 +410,6 @@ \section{Hardly ramified representations} \begin{theorem}\label{Frey_curve_irreducible} The $\ell$-torsion in the Frey curve associated to a Frey package $(a,b,c,\ell)$ is irreducible. \end{theorem} -\begin{proof}\uses{Frey_curve_reducible_structure, Frey_curve_no_trivial_submodule, Frey_curve_no_trivial_quotient,EllipticCurve.n_torsion_dimension} Follows from theorem~\ref{Frey_curve_reducible_structure}, corollary~\ref{Frey_curve_no_trivial_submodule} +\begin{proof}\uses{Frey_curve_reducible_structure, Frey_curve_no_trivial_submodule, Frey_curve_no_trivial_quotient,Elliptic_curve_n_torsion_2d} Follows from theorem~\ref{Frey_curve_reducible_structure}, corollary~\ref{Frey_curve_no_trivial_submodule} and corollary~\ref{Frey_curve_no_trivial_quotient}. \end{proof}