better

leanprover-community · Mar 4, 2024 · 3727a95 · 3727a95
1 parent d9a41fc
commit 3727a95
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/FltRegular/FLT5.lean b/FltRegular/FLT5.lean
@@ -1,8 +1,7 @@
 import Mathlib
 import FltRegular
 
-open Nat NumberField Polynomial IsPrimitiveRoot IsCyclotomicExtension Real Complex
-open scoped nonZeroDivisors
+open Nat NumberField IsCyclotomicExtension
 
 theorem fermatLastTheoremFive : FermatLastTheoremFor 5 := by
   have : Fact (Nat.Prime 5) := ⟨by norm_num⟩