remove Dickson

leanprover-community · Sep 11, 2024 · bb46d41 · bb46d41
1 parent 7fe6c4f
commit bb46d41
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 323 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2432,7 +2432,6 @@ import Mathlib.Data.Option.Basic
 import Mathlib.Data.Option.Defs
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Ordering.Basic
-import Mathlib.Data.Ordering.Dickson
 import Mathlib.Data.Ordering.Lemmas
 import Mathlib.Data.Ordmap.Ordnode
 import Mathlib.Data.Ordmap.Ordset

diff --git a/Mathlib/Data/Ordering/Dickson.lean b/Mathlib/Data/Ordering/Dickson.lean