tests

ChrisHughes24 · Apr 1, 2019 · 490c75f · 490c75f
1 parent fd3e494
commit 490c75f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/data/padics/hensel.lean b/src/data/padics/hensel.lean
@@ -416,3 +416,5 @@ lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.deriv
 if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else
 by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _, soln_unique _ _⟩;
    assumption
+
+lemma aghk : true := trivial