Commit 1a6f1468 authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

removed irrelevant comments in chapter 5

parent 75f36f16
......@@ -550,10 +550,6 @@ $M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{
As direct consequence, using \lref{lemma:curve-or-twist}, we prove that for all
$x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on
$M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.
%for that you don't need that lemma, because in \F{p^2} you have square roots
%what you mean is that those points always are either from the curve or from th e twist in \F{p}
%do you have that as a lemma too?
%if so that lemma is what should be here
\begin{lstlisting}[language=Coq]
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment