From 3727a95f7975eb25a465c9024ab40045d92b5407 Mon Sep 17 00:00:00 2001
From: riccardobrasca <riccardo.brasca@gmail.com>
Date: Mon, 4 Mar 2024 12:08:02 +0100
Subject: [PATCH] better

---
 FltRegular/FLT5.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/FltRegular/FLT5.lean b/FltRegular/FLT5.lean
index 16d2c71c..d46650e2 100644
--- 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⟩