compatible family is not \leanok because lean code not yet in the repo

Author: kbuzzard

blueprint/src/chapter/chtopbestiary.tex

@@ -205,7 +205,7 @@ \section{Galois representations}
 representations, modulo the existence of Frobenius elements, which has been
 established by Jou Glasheen. 
 
-\begin{definition}\label{compatible_family}\leanok Let $N$ be a number field. A \emph{compatible family of $d$-dimensional Galois representations over $N$} is a finite set of finite places $S$ of $N$,
+\begin{definition}\label{compatible_family} Let $N$ be a number field. A \emph{compatible family of $d$-dimensional Galois representations over $N$} is a finite set of finite places $S$ of $N$,
 a number field $E$, a monic degree $d$ polynomial $F_{\p}(X)\in E[X]$ for each finite place $\p$ of $K$ not in $S$ and, for each prime number $\ell$ and field embedding $\phi : E\to\Qlbar$ (or essentially equivalently for each finite place of $E$), a continuous homomorphism $\rho:\GK\to\GL_2(\Qlbar)$ unramified outside $S$ and the primes of $K$ above $\ell$, such that $\rho(\Frob_\p)$ has characteristic polynomial $P_\pi(X)$ if $\pi$ lies above a prime number $p\not=\ell$ with $p\not\in S$.
 \end{definition}