add some latex for chapter 2

mo271 · Sep 22, 2024 · f558e1f · f558e1f
1 parent 63c63b6
commit f558e1f
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 3 deletions.
diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean
@@ -15,7 +15,6 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Data.Nat.Choose.Factorization
@@ -38,7 +37,7 @@ formalized by Patrick Stevens and Bolton Bailey.
 -/
 open scoped BigOperators
 
-namespace chapter02
+namespace chapter2
 
 open Real
 
@@ -226,4 +225,4 @@ theorem exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) :
 
 
 
-end chapter02
+end chapter2
diff --git a/blueprint/src/chapter/chapter02.tex b/blueprint/src/chapter/chapter02.tex
@@ -1 +1,13 @@
 \chapter{Bertrand's postulate}
+
+\begin{theorem}
+    \label{thm:bertrands_postulate}
+    \lean{chapter2.exists_prime_lt_and_le_two_mul}
+    \leanok
+    For any positive natural number, there is a prime which is greater than
+    it, but no more than twice as large.
+\end{theorem}
+\begin{proof}
+    \leanok
+    TODO: make this follow the book proof more closely!
+\end{proof}