diff --git a/FirstCourseAbstractAlgebra.lean b/FirstCourseAbstractAlgebra.lean index 764aaee..17778be 100644 --- a/FirstCourseAbstractAlgebra.lean +++ b/FirstCourseAbstractAlgebra.lean @@ -1 +1 @@ -import FirstCourseAbstractAlgebra.Chapter1 \ No newline at end of file +import FirstCourseAbstractAlgebra.Fraleigh \ No newline at end of file diff --git a/FirstCourseAbstractAlgebra/Fraleigh.lean b/FirstCourseAbstractAlgebra/Fraleigh.lean new file mode 100644 index 0000000..c0d0c22 --- /dev/null +++ b/FirstCourseAbstractAlgebra/Fraleigh.lean @@ -0,0 +1 @@ +import FirstCourseAbstractAlgebra.Fraleigh.Chapter1 \ No newline at end of file diff --git a/FirstCourseAbstractAlgebra/Chapter1.lean b/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean similarity index 100% rename from FirstCourseAbstractAlgebra/Chapter1.lean rename to FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean diff --git a/MathematicalIntroductionLogic.lean b/MathematicalIntroductionLogic.lean index 6462279..bb841aa 100644 --- a/MathematicalIntroductionLogic.lean +++ b/MathematicalIntroductionLogic.lean @@ -1,2 +1,2 @@ -import MathematicalIntroductionLogic.Chapter0 +import MathematicalIntroductionLogic.Enderton import MathematicalIntroductionLogic.Tuple \ No newline at end of file diff --git a/MathematicalIntroductionLogic/Enderton.lean b/MathematicalIntroductionLogic/Enderton.lean new file mode 100644 index 0000000..c2fb97c --- /dev/null +++ b/MathematicalIntroductionLogic/Enderton.lean @@ -0,0 +1 @@ +import MathematicalIntroductionLogic.Enderton.Chapter0 \ No newline at end of file diff --git a/MathematicalIntroductionLogic/Chapter0.lean b/MathematicalIntroductionLogic/Enderton/Chapter0.lean similarity index 100% rename from MathematicalIntroductionLogic/Chapter0.lean rename to MathematicalIntroductionLogic/Enderton/Chapter0.lean diff --git a/MathematicalIntroductionLogic/Chapter0.tex b/MathematicalIntroductionLogic/Enderton/Chapter0.tex similarity index 100% rename from MathematicalIntroductionLogic/Chapter0.tex rename to MathematicalIntroductionLogic/Enderton/Chapter0.tex diff --git a/OneVariableCalculus.lean b/OneVariableCalculus.lean index 8229284..95d20f4 100644 --- a/OneVariableCalculus.lean +++ b/OneVariableCalculus.lean @@ -1,3 +1,2 @@ -import OneVariableCalculus.Chapters -import OneVariableCalculus.Exercises +import OneVariableCalculus.Apostol import OneVariableCalculus.Real \ No newline at end of file diff --git a/OneVariableCalculus/Apostol.lean b/OneVariableCalculus/Apostol.lean new file mode 100644 index 0000000..55a224e --- /dev/null +++ b/OneVariableCalculus/Apostol.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Apostol.Chapter_I_3 +import OneVariableCalculus.Apostol.Exercises_1_7 +import OneVariableCalculus.Apostol.Exercises_I_3_12 \ No newline at end of file diff --git a/OneVariableCalculus/Chapters/Chapter_I_3.lean b/OneVariableCalculus/Apostol/Chapter_I_3.lean similarity index 100% rename from OneVariableCalculus/Chapters/Chapter_I_3.lean rename to OneVariableCalculus/Apostol/Chapter_I_3.lean diff --git a/OneVariableCalculus/Chapters/Chapter_I_3.tex b/OneVariableCalculus/Apostol/Chapter_I_3.tex similarity index 100% rename from OneVariableCalculus/Chapters/Chapter_I_3.tex rename to OneVariableCalculus/Apostol/Chapter_I_3.tex diff --git a/OneVariableCalculus/Exercises/Exercises_1_7.lean b/OneVariableCalculus/Apostol/Exercises_1_7.lean similarity index 100% rename from OneVariableCalculus/Exercises/Exercises_1_7.lean rename to OneVariableCalculus/Apostol/Exercises_1_7.lean diff --git a/OneVariableCalculus/Exercises/Exercises_I_3_12.lean b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean similarity index 99% rename from OneVariableCalculus/Exercises/Exercises_I_3_12.lean rename to OneVariableCalculus/Apostol/Exercises_I_3_12.lean index 921f7fc..b4538c0 100644 --- a/OneVariableCalculus/Exercises/Exercises_I_3_12.lean +++ b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean @@ -10,7 +10,7 @@ import Mathlib.Data.Real.Sqrt import Mathlib.Tactic.LibrarySearch import Bookshelf.Real.Rational -import OneVariableCalculus.Chapters.Chapter_I_3 +import OneVariableCalculus.Apostol.Chapter_I_3 -- ======================================== -- Exercise 1 diff --git a/OneVariableCalculus/Chapters.lean b/OneVariableCalculus/Chapters.lean deleted file mode 100644 index 9a2293a..0000000 --- a/OneVariableCalculus/Chapters.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Chapters.Chapter_I_3 \ No newline at end of file diff --git a/OneVariableCalculus/Exercises.lean b/OneVariableCalculus/Exercises.lean deleted file mode 100644 index 9e6a5bc..0000000 --- a/OneVariableCalculus/Exercises.lean +++ /dev/null @@ -1,2 +0,0 @@ -import OneVariableCalculus.Exercises.Exercises_I_3_12 -import OneVariableCalculus.Exercises.Exercises_1_7 \ No newline at end of file diff --git a/TheoremProvingInLean.lean b/TheoremProvingInLean.lean index edb8563..07435c6 100644 --- a/TheoremProvingInLean.lean +++ b/TheoremProvingInLean.lean @@ -1,6 +1 @@ -import TheoremProvingInLean.Chapter2 -import TheoremProvingInLean.Chapter3 -import TheoremProvingInLean.Chapter4 -import TheoremProvingInLean.Chapter5 -import TheoremProvingInLean.Chapter7 -import TheoremProvingInLean.Chapter8 +import TheoremProvingInLean.Avigad diff --git a/TheoremProvingInLean/Avigad.lean b/TheoremProvingInLean/Avigad.lean new file mode 100644 index 0000000..7b091f1 --- /dev/null +++ b/TheoremProvingInLean/Avigad.lean @@ -0,0 +1,6 @@ +import TheoremProvingInLean.Avigad.Chapter2 +import TheoremProvingInLean.Avigad.Chapter3 +import TheoremProvingInLean.Avigad.Chapter4 +import TheoremProvingInLean.Avigad.Chapter5 +import TheoremProvingInLean.Avigad.Chapter7 +import TheoremProvingInLean.Avigad.Chapter8 diff --git a/TheoremProvingInLean/Chapter2.lean b/TheoremProvingInLean/Avigad/Chapter2.lean similarity index 100% rename from TheoremProvingInLean/Chapter2.lean rename to TheoremProvingInLean/Avigad/Chapter2.lean diff --git a/TheoremProvingInLean/Chapter3.lean b/TheoremProvingInLean/Avigad/Chapter3.lean similarity index 100% rename from TheoremProvingInLean/Chapter3.lean rename to TheoremProvingInLean/Avigad/Chapter3.lean diff --git a/TheoremProvingInLean/Chapter4.lean b/TheoremProvingInLean/Avigad/Chapter4.lean similarity index 100% rename from TheoremProvingInLean/Chapter4.lean rename to TheoremProvingInLean/Avigad/Chapter4.lean diff --git a/TheoremProvingInLean/Chapter5.lean b/TheoremProvingInLean/Avigad/Chapter5.lean similarity index 100% rename from TheoremProvingInLean/Chapter5.lean rename to TheoremProvingInLean/Avigad/Chapter5.lean diff --git a/TheoremProvingInLean/Chapter7.lean b/TheoremProvingInLean/Avigad/Chapter7.lean similarity index 100% rename from TheoremProvingInLean/Chapter7.lean rename to TheoremProvingInLean/Avigad/Chapter7.lean diff --git a/TheoremProvingInLean/Chapter8.lean b/TheoremProvingInLean/Avigad/Chapter8.lean similarity index 100% rename from TheoremProvingInLean/Chapter8.lean rename to TheoremProvingInLean/Avigad/Chapter8.lean