Restructure the lemmas and definitions

Generalize some lemmas a little
metinersin · Aug 16, 2024 · 8cb297e · 8cb297e
1 parent 53bb91a
commit 8cb297e
Show file tree

Hide file tree

Showing 21 changed files with 1,700 additions and 472 deletions.
diff --git a/FormalTextbookModelTheory.lean b/FormalTextbookModelTheory.lean
@@ -1,2 +1,3 @@
-import FormalTextbookModelTheory.ForMathlib.Matrix
-import FormalTextbookModelTheory.ForMathlib.DLO
+import FormalTextbookModelTheory.ForMathlib.Data.Fin.VecNotation
+import FormalTextbookModelTheory.ForMathlib.ModelTheory.Order
+import FormalTextbookModelTheory.ForMathlib.ModelTheory.DLO
diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean
diff --git a/...extbookModelTheory/ForMathlib/Matrix.lean → ...eory/ForMathlib/Data/Fin/VecNotation.lean b/...extbookModelTheory/ForMathlib/Matrix.lean → ...eory/ForMathlib/Data/Fin/VecNotation.lean