Comment out unfinished proof in Frobenius2.lean

ImperialCollegeLondon · Jun 23, 2024 · ca08f2e · ca08f2e
1 parent 39a3620
commit ca08f2e
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean
@@ -342,11 +342,11 @@ lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸
     change (Frob A Q isGalois P) • x - _ ∈ _
     rw [← smul_sub]
     nth_rw 3 [ ← fact3]
-    suffices (x - y A Q ^ n) ∈ Q by
-      exact?
-    rw [smul_mem_smul]
-    simp
-    skip
+    -- suffices (x - y A Q ^ n) ∈ Q by
+    --   exact?
+    -- rw [smul_mem_smul]
+    -- simp
+    -- skip
     sorry
 
 /- maths proof: