initial test

leanprover-community · Sep 26, 2024 · 78199af · 78199af
1 parent 8fdf59c
commit 78199af
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3475,6 +3475,7 @@ import Mathlib.NumberTheory.Zsqrtd.Basic
 import Mathlib.NumberTheory.Zsqrtd.GaussianInt
 import Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
 import Mathlib.NumberTheory.Zsqrtd.ToReal
+import Mathlib.Numerology.Everything
 import Mathlib.Order.Antichain
 import Mathlib.Order.Antisymmetrization
 import Mathlib.Order.Atoms

diff --git a/Mathlib/Numerology/Everything.lean b/Mathlib/Numerology/Everything.lean