chore(Periodic): reduce imports

leanprover-community · Jan 13, 2025 · 1e38c62 · 1e38c62
1 parent 3c1ea2e
commit 1e38c62
Show file tree

Hide file tree

Showing 2 changed files with 423 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -913,6 +913,7 @@ import Mathlib.Algebra.Ring.Nat
 import Mathlib.Algebra.Ring.NegOnePow
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Algebra.Ring.Parity
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.Algebra.Ring.Pointwise.Finset
 import Mathlib.Algebra.Ring.Pointwise.Set