fix last of broken references

Author: kbuzzard

blueprint/src/chapter/ch02reductions.tex

@@ -125,8 +125,8 @@ \section{Reduction to two big theorems.}
 \begin{proof}\uses{Frey_curve_irreducible}\tangled This follows from a profound result of Mazur \cite{mazur-torsion} from 1979, namely the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact a fair amount of work still needs to be done to deduce the theorem from Mazur's result. We will have more to say about this result later.
 \end{proof}
 
-\begin{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\label{FLT.FreyCurve.Wiles_Frey}\lean{FLT.FreyCurve.Wiles_Frey}\uses{FLT.FreyCurve.mod_p_Galois_representation, modularity_lifting_theorem}\leanok $\rho$ cannot be irreducible either.\end{theorem}
-\begin{proof}\uses{Frey_mod_p_Galois_representation, frey_curve_hardly_ramified}\tangled This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this.
+\begin{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\label{FLT.FreyCurve.Wiles_Frey}\lean{FLT.FreyCurve.Wiles_Frey}\uses{FLT.FreyCurve.mod_p_Galois_representation}\leanok $\rho$ cannot be irreducible either.\end{theorem}
+\begin{proof}\uses{modularity_lifting_theorem,frey_curve_hardly_ramified}\tangled This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this.
 \end{proof}
 
 \begin{corollary}\label{FLT.Frey_package.false}\lean{FLT.Frey_package.false}\uses{FLT.FreyCurve.Mazur_Frey, FLT.FreyCurve.Wiles_Frey}\leanok There is no Frey package.\end{corollary}

blueprint/src/chapter/ch03frey.tex

@@ -10,7 +10,7 @@ \section{The arithmetic of elliptic curves}
 We give an overview of the results we need, citing the literature for proofs. Everything here is
  standard, and mostof it dates back to the 1970s or before.
 
-\begin{theorem}\label{EllipticCurve.torsion_card}\lean{EllipticCurve.n_torsion_card}\tangled
+\begin{theorem}\label{EllipticCurve.n_torsion_card}\lean{EllipticCurve.n_torsion_card}\tangled
   Let $n$ be a positive integer, let $F$ be a separably closed
   field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(K)[n]$ 
   in the $F$-points of $E$ is a finite group of size $n^2$.