Blueprint: IsDedekindDomain.HeightOneSpectrum.valuation_comap is done (…

…#216)
ImperialCollegeLondon · Nov 13, 2024 · 7f9ccb8 · 7f9ccb8
1 parent 2473f61
commit 7f9ccb8
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/blueprint/src/chapter/AdeleMiniproject.tex b/blueprint/src/chapter/AdeleMiniproject.tex
@@ -132,7 +132,8 @@ \section{Results about finite adeles which we can work on now}
   \lean{IsDedekindDomain.HeightOneSpectrum.valuation_comap}
 \end{lemma}
 \begin{proof}
-   Standard.
+  \leanok
+  Standard.
 \end{proof}
 
 \begin{definition}