diff --git a/.gitignore b/.gitignore
index 7934deda..db8a47ff 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,11 +3,14 @@
 /lake-packages/*
 .lake/*
 .DS_Store
+# Lean blueprint
 blueprint/print/print.log
 blueprint/web/
+blueprint/src/web.paux
+blueprint/src/web.bbl
 blueprint/print/
 # KB guesses this is safe (he's asked Patrick)
-blueprint/lean_decls
+blueprint/lean_decls 
 # Files generated by LaTeX
 *.aux
 *.bbl
@@ -18,4 +21,5 @@ blueprint/lean_decls
 *.fls
 *.fdb_latexmk
 *.synctex.gz
-
+# Python virtual environment 
+/.venv
\ No newline at end of file
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}