From 947d2f4c01ee6f3ece969f87f5e4b9aa8f453e77 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 26 Apr 2023 15:44:52 -0600 Subject: [PATCH] Revert to nesting author names. These modules group together chapter/exercise specific proofs vs. concepts that permeate said chapters. --- FirstCourseAbstractAlgebra.lean | 2 +- FirstCourseAbstractAlgebra/Fraleigh.lean | 1 + FirstCourseAbstractAlgebra/{ => Fraleigh}/Chapter1.lean | 0 MathematicalIntroductionLogic.lean | 2 +- MathematicalIntroductionLogic/Enderton.lean | 1 + MathematicalIntroductionLogic/{ => Enderton}/Chapter0.lean | 0 MathematicalIntroductionLogic/{ => Enderton}/Chapter0.tex | 0 OneVariableCalculus.lean | 3 +-- OneVariableCalculus/Apostol.lean | 3 +++ OneVariableCalculus/{Chapters => Apostol}/Chapter_I_3.lean | 0 OneVariableCalculus/{Chapters => Apostol}/Chapter_I_3.tex | 0 .../{Exercises => Apostol}/Exercises_1_7.lean | 0 .../{Exercises => Apostol}/Exercises_I_3_12.lean | 2 +- OneVariableCalculus/Chapters.lean | 1 - OneVariableCalculus/Exercises.lean | 2 -- TheoremProvingInLean.lean | 7 +------ TheoremProvingInLean/Avigad.lean | 6 ++++++ TheoremProvingInLean/{ => Avigad}/Chapter2.lean | 0 TheoremProvingInLean/{ => Avigad}/Chapter3.lean | 0 TheoremProvingInLean/{ => Avigad}/Chapter4.lean | 0 TheoremProvingInLean/{ => Avigad}/Chapter5.lean | 0 TheoremProvingInLean/{ => Avigad}/Chapter7.lean | 0 TheoremProvingInLean/{ => Avigad}/Chapter8.lean | 0 23 files changed, 16 insertions(+), 14 deletions(-) create mode 100644 FirstCourseAbstractAlgebra/Fraleigh.lean rename FirstCourseAbstractAlgebra/{ => Fraleigh}/Chapter1.lean (100%) create mode 100644 MathematicalIntroductionLogic/Enderton.lean rename MathematicalIntroductionLogic/{ => Enderton}/Chapter0.lean (100%) rename MathematicalIntroductionLogic/{ => Enderton}/Chapter0.tex (100%) create mode 100644 OneVariableCalculus/Apostol.lean rename OneVariableCalculus/{Chapters => Apostol}/Chapter_I_3.lean (100%) rename OneVariableCalculus/{Chapters => Apostol}/Chapter_I_3.tex (100%) rename OneVariableCalculus/{Exercises => Apostol}/Exercises_1_7.lean (100%) rename OneVariableCalculus/{Exercises => Apostol}/Exercises_I_3_12.lean (99%) delete mode 100644 OneVariableCalculus/Chapters.lean delete mode 100644 OneVariableCalculus/Exercises.lean create mode 100644 TheoremProvingInLean/Avigad.lean rename TheoremProvingInLean/{ => Avigad}/Chapter2.lean (100%) rename TheoremProvingInLean/{ => Avigad}/Chapter3.lean (100%) rename TheoremProvingInLean/{ => Avigad}/Chapter4.lean (100%) rename TheoremProvingInLean/{ => Avigad}/Chapter5.lean (100%) rename TheoremProvingInLean/{ => Avigad}/Chapter7.lean (100%) rename TheoremProvingInLean/{ => Avigad}/Chapter8.lean (100%) 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