Minimalize import

ImperialCollegeLondon · Nov 25, 2023 · e017f8c · e017f8c
1 parent 6a20383
commit e017f8c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/FLT.lean b/FLT.lean
@@ -1,4 +1,4 @@
-import Mathlib
+import Mathlib.Data.PNat.Basic
 
 theorem PNat.pow_add_pow_ne_pow
  (x y z : ℕ+)