From 78199af5ee01c8d450dce7790a7e85c4c2c5d0df Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 26 Sep 2024 15:06:24 +0200 Subject: [PATCH] initial test --- Mathlib.lean | 1 + Mathlib/Numerology/Everything.lean | 0 2 files changed, 1 insertion(+) create mode 100644 Mathlib/Numerology/Everything.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3442f8704e094..ddf844378e225 100644 --- 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 new file mode 100644 index 0000000000000..e69de29bb2d1d