fix

leanprover-community · Feb 1, 2025 · b303e92 · b303e92
1 parent fe1d8e0
commit b303e92
Show file tree

Hide file tree

Showing 6 changed files with 1 addition and 11 deletions.
diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Algebra.ModEq
-import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Data.Int.SuccPred
 import Mathlib.Order.Circular
-import Mathlib.Data.List.TFAE
-import Mathlib.Data.Set.Lattice
 
 /-!
 # Reducing to an interval modulo its length

diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.Field.NegOnePow
 import Mathlib.Algebra.Field.Periodic
 import Mathlib.Algebra.QuadraticDiscriminant
 import Mathlib.Analysis.SpecialFunctions.Exp
-import Mathlib.Tactic.Positivity.Core
 
 /-!
 # Trigonometric functions

diff --git a/Mathlib/Data/Nat/Periodic.lean b/Mathlib/Data/Nat/Periodic.lean
@@ -5,8 +5,6 @@ Authors: Bolton Bailey
 -/
 import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Data.Nat.Count
-import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Order.Interval.Finset.Nat
 
 /-!
 # Periodic Functions on ℕ

diff --git a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
@@ -6,7 +6,6 @@ Authors: Chris Hughes
 import Mathlib.Algebra.Algebra.ZMod
 import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.MvPolynomial.Cardinal
-import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.RingTheory.Algebraic.Cardinality
 import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

diff --git a/Mathlib/GroupTheory/Perm/Centralizer.lean b/Mathlib/GroupTheory/Perm/Centralizer.lean
@@ -3,17 +3,13 @@ Copyright (c) 2023 Antoine Chambert-Loir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
-
 import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.NoncommCoprod
-import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.GroupTheory.Perm.ConjAct
-import Mathlib.GroupTheory.Perm.Cycle.Factors
 import Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
 import Mathlib.GroupTheory.Perm.DomMulAct
-import Mathlib.GroupTheory.Perm.Finite
 
 /-! # Centralizer of a permutation and cardinality of conjugacy classes
   # in the symmetric groups

diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
@@ -6,6 +6,7 @@ Authors: Johan Commelin, Chris Hughes
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.GroupTheory.SpecificGroups.Cyclic
+import Mathlib.Tactic.FieldSimp
 
 /-!
 # Integral domains