Commit 2025-11-14 16:11 7e683ccc

View on Github →

chore: remove some superfluous imports (#31616)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Center.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Algebra/Group/Nat/Hom.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

Modified Mathlib/Algebra/Opposites.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/Quantale.lean

Modified Mathlib/Algebra/PEmptyInstances.lean

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Nat/Cast/Defs.lean

Modified Mathlib/Data/Nat/Find.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Tactic/Measurability.lean

Modified Mathlib/Topology/Algebra/Semigroup.lean

Modified Mathlib/Topology/Order/LocalExtr.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean