ch6: remove test

mo271 · Oct 13, 2023 · 7ca0042 · 7ca0042
1 parent 417789c
commit 7ca0042
Showing 1 changed file with 0 additions and 11 deletions.
diff --git a/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean b/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean
@@ -115,17 +115,6 @@ theorem h_lamb_gt_q_sub_one (q n : ℕ) (lamb : ℂ):
   simp only [norm_eq_abs, map_nonneg, Real.sqrt_sq] at g
   exact g
 
-
-
-
-lemma test' (b : ℕ): (a : ℕ) → a = b := by
-  sorry
-
-lemma test (b : ℕ) (a : ℕ) : a = b := by
-  have := test' b
-
-  sorry
-
 lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
     (H : q ^ k - 1 ∣ q ^ n - 1) : k ∣ n := by
   revert H