diff --git a/.gitignore b/.gitignore
index 61892570..c76964ca 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,7 @@ blueprint/web/
 blueprint/src/web.paux
 blueprint/src/web.bbl
 blueprint/print/
+blueprint/lean_decls
 # Files generated by LaTeX
 *.aux
 *.bbl
@@ -18,4 +19,4 @@ blueprint/print/
 *.pdf
 *.fls
 *.fdb_latexmk
-*.synctex.gz
\ No newline at end of file
+*.synctex.gz
diff --git a/blueprint/src/chapter/ch02reductions.tex b/blueprint/src/chapter/ch02reductions.tex
index 7956b4aa..3e384e40 100644
--- a/blueprint/src/chapter/ch02reductions.tex
+++ b/blueprint/src/chapter/ch02reductions.tex
@@ -69,21 +69,21 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
 
 The group structure behaves well under change of field.
 
-\begin{lemma}\label{EllipticCurve.Points.map}\lean{EllipticCurve.Points.map}\leanok If $E$ is an elliptic curve over a field $k$, and if $K$ and $L$ are two fields which are $k$-algebras, and if $f:K\to L$ is a $k$-algebra homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism.
+\begin{lemma}\label{WeierstrassCurve.Points.map}\lean{WeierstrassCurve.Points.map}\leanok If $E$ is an elliptic curve over a field $k$, and if $K$ and $L$ are two fields which are $k$-algebras, and if $f:K\to L$ is a $k$-algebra homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism.
 \end{lemma}
 \begin{proof} The equations defining the group law are ratios of polynomials with coefficients in $k$, and such things behave well under $k$-algebra homomorphisms.
 \end{proof}
 
 This construction is functorial (it sends the identity to the identity, and compositions to compositions).
 
-\begin{lemma}\label{EllipticCurve.Points.map_id}\lean{EllipticCurve.Points.map_id}\uses{EllipticCurve.Points.map}
+\begin{lemma}\label{WeierstrassCurve.Points.map_id}\lean{WeierstrassCurve.Points.map_id}\uses{WeierstrassCurve.Points.map}
   The group homomorphism $E(K)\to E(K)$ induced by the identity map $K\to K$ is the
   identity group homomorphism.
 \end{lemma}
 \begin{proof} An easy calculation.
 \end{proof}
 
-\begin{lemma}\label{EllipticCurve.Points.map_comp}\lean{EllipticCurve.Points.map_comp}\uses{EllipticCurve.Points.map}
+\begin{lemma}\label{WeierstrassCurve.Points.map_comp}\lean{WeierstrassCurve.Points.map_comp}\uses{WeierstrassCurve.Points.map}
   If $K\to L\to M$ are $k$-algebra homomorphisms then the group homomorphism $E(K)\to E(M)$
   induced by the map $K\to M$ is the composite of the map $E(K)\to E(L)$ induced by $K\to L$
   and the map $E(L)\to E(M)$ induced by the map $L\to M$.
@@ -93,7 +93,7 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
 
  Thus if $f:K\to L$ is an isomorphism of fields, the induced map $E(K)\to E(L)$ is an isomorphism of groups, with the inverse isomorphism being the map $E(L)\to E(K)$ induced by $f^{-1}$. This construction thus gives us an action of the multiplicative group $\Aut_k(K)$ of automorphisms of the field $K$ on the additive abelian group $E(K)$.
 
-\begin{definition}\label{EllipticCurve.galoisRepresentation}\lean{EllipticCurve.galoisRepresentation}\uses{EllipticCurve.Points.map_id,EllipticCurve.Points.map_comp}
+\begin{definition}\label{WeierstrassCurve.galoisRepresentation}\lean{WeierstrassCurve.galoisRepresentation}\uses{WeierstrassCurve.Points.map_id,WeierstrassCurve.Points.map_comp}
   If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
   then the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)$.
 \end{definition}
@@ -101,7 +101,7 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
 
 We need a variant of this construction where we only consider the $n$-torsion of the curve, for $n$ a positive integer. Recall that if $A$ is any additive abelian group, and if $n$ is a positive integer, then we can consider the subgroup $A[n]$ of elements $a$ such that $na=0$. If a group~$G$ acts on $A$ via additive group isomorphisms, then there will be an induced action of~$G$ on $A[n]$.
 
-\begin{definition}\label{EllipticCurve.torsionGaloisRepresentation}\lean{EllipticCurve.torsionGaloisRepresentation}\uses{EllipticCurve.galoisRepresentation}
+\begin{definition}\label{WeierstrassCurve.torsionGaloisRepresentation}\lean{WeierstrassCurve.torsionGaloisRepresentation}\uses{WeierstrassCurve.galoisRepresentation}
   If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
   and if $n$ is a natural number, then the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)[n]$ of $n$-torsion points on the curve.
 \end{definition}
diff --git a/blueprint/src/chapter/ch03frey.tex b/blueprint/src/chapter/ch03frey.tex
index 7cdbe5ed..0c8d219b 100644
--- a/blueprint/src/chapter/ch03frey.tex
+++ b/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 most of it dates back to the 1970s or before.
 
-\begin{theorem}\label{EllipticCurve.n_torsion_card}\lean{EllipticCurve.n_torsion_card}\notready
+\begin{theorem}\label{WeierstrassCurve.n_torsion_card}\lean{WeierstrassCurve.n_torsion_card}\notready
   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$.
@@ -29,14 +29,14 @@ \section{The arithmetic of elliptic curves}
   with $a_i\mid a_{i+1}$ (this is possible by the structure theorem for finite abelian groups), and then to apply our hypothesis firstly with $d=a_1$ to deduce $t=r$ and then with $d=a_t$ to deduce $a_1=a_t$.
 \end{proof}
 
-\begin{corollary}\label{Elliptic_curve_n_torsion_2d}\lean{EllipticCurve.n_torsion_dimension}
+\begin{corollary}\label{Elliptic_curve_n_torsion_2d}\lean{WeierstrassCurve.n_torsion_dimension}
   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(F)[n]$
   in the $F$-points of $E$ is a finite group isomorphic to $(\Z/n\Z)^2$.
 \end{corollary}
-\begin{proof}\uses{group_theory_lemma,EllipticCurve.n_torsion_card}
+\begin{proof}\uses{group_theory_lemma,WeierstrassCurve.n_torsion_card}
   This follows from the previous group-theoretic lemma~\ref{group_theory_lemma} and
-  theorem~\ref{EllipticCurve.n_torsion_card}.
+  theorem~\ref{WeierstrassCurve.n_torsion_card}.
 \end{proof}
 
 We saw in section~\ref{twopointfour} that if $E$ is an elliptic curve over a field $k$ and if $k^{\sep}$ is a separable closure of~$k$, then the group $\Gal(k^{\sep}/k)$ acts on $E(k^{\sep})[n]$. Now let $n$ be a positive integer which is nonzero in $k$. We have just seen that $E(k^{\sep})[n]$ is isomorphic to $(\Z/n\Z)^2$, and it inherits an action of $\Gal(k^{\sep}/k)$. If we fix an isomorphism $E(k^{\sep})[n]\cong(\Z/n\Z)^2$ then we get a representation $\Gal(k^{\sep}/k)\to\GL_2(\Z/n\Z)$. A fundamental fact about this Galois representation is that its determinant is the cyclotomic character.