diff --git a/Mathlib/Algebra/Ring/NegOnePow.lean b/Mathlib/Algebra/Ring/NegOnePow.lean index 1de416d1d42c5a..194d23e68cc1a4 100644 --- a/Mathlib/Algebra/Ring/NegOnePow.lean +++ b/Mathlib/Algebra/Ring/NegOnePow.lean @@ -6,7 +6,6 @@ Authors: Joël Riou, Johan Commelin import Mathlib.Algebra.Ring.Int.Parity import Mathlib.Algebra.Ring.Int.Units import Mathlib.Data.ZMod.IntUnitsPower -import Mathlib.Tactic.NormNum /-! # Integer powers of (-1)