Rename all chapters (#57)

Could be reverted when https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Weird.20filenames.20and.20doc4-gen
is resolved.

Author: mo271

FormalBook.lean

@@ -1,46 +1,45 @@
-import FormalBook.Ch01_Six_proofs_of_the_infinity_of_primes
-import FormalBook.«Ch02_Bertrand's_postulate»
-import FormalBook.«Ch03_Binomial_coefficients_are_(almost)_never_powers»
-import FormalBook.Ch04_Representing_numbers_as_sums_of_two_squares
-import FormalBook.Ch05_The_law_of_quadratic_reciprocity
-import FormalBook.Ch06_Every_finite_division_ring_is_a_field
-import FormalBook.«Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem»
-import FormalBook.Ch08_Some_irrational_numbers
-import FormalBook.«Ch09_Four_times_pi²_over_6»
-import FormalBook.«Ch10_Hilbert's_third_problem_decomposing_polyhedra»
-import FormalBook.Ch11_Lines_in_the_plane_and_decompositions_of_graphs
-import FormalBook.Ch12_The_slope_problem
-import FormalBook.«Ch13_Three_applications_of_Euler's_formula»
-import FormalBook.«Ch14_Cauchy's_rigidity_theorem»
-import FormalBook.«Ch15_The_Borromean_rings_don't_exist»
-import FormalBook.Ch16_Touching_simplices
-import FormalBook.Ch17_Every_large_point_set_has_an_obtuse_angle
-import FormalBook.«Ch18_Borsuk's_conjecture»
-import FormalBook.«Ch19_Sets,_functions,_and_the_continuum_hypothesis»
-import FormalBook.Ch20_In_praise_of_inequalities
-import FormalBook.Ch21_The_fundamental_theorem_of_algebra
-import FormalBook.Ch22_One_square_and_an_odd_number_of_triangles
-import FormalBook.«Ch23_A_theorem_of_Pólya_on_polynomials»
-import FormalBook.«Ch24_Van_der_Waerden's_permanent_conjecture»
-import FormalBook.Ch25_On_a_lemma_of_Littlewook_and_Offord
-import FormalBook.Ch26_Cotangent_and_the_Herglotz_trick
-import FormalBook.«Ch27_Buffon's_needle_problem»
-import FormalBook.«Ch28_Pigeon-hole_and_double_counting»
-import FormalBook.Ch29_Tiling_rectangles
-import FormalBook.Ch30_Three_famous_theorems_on_finite_sets
-import FormalBook.Ch31_Shuffling_cards
-import FormalBook.«Ch33_Cayley's_formula_for_the_number_of_trees»
-import FormalBook.Ch32_Lattice_paths_and_determinants
-import FormalBook.Ch34_Identities_versus_bijections
-import FormalBook.Ch35_The_finite_Kakeya_problem
-import FormalBook.Ch36_Completing_Latin_squares
-import FormalBook.Ch37_Permanents_and_the_power_of_entropy
-import FormalBook.Ch38_The_Dinitz_problem
-import FormalBook.«Ch39_Five-coloring_plane_graphs»
-import FormalBook.Ch40_How_to_guard_a_museum
-import FormalBook.«Ch41_Turán's_graph_theorem»
-import FormalBook.Ch42_Communicating_without_errors
-import FormalBook.Ch43_The_chromatic_number_of_Kneser_graphs
-import FormalBook.Ch44_Of_friends_and_politicians
-import FormalBook.«Ch45_Probability_makes_counting_(sometimes)_easy»
-
+import FormalBook.Chapter_01
+import FormalBook.Chapter_02
+import FormalBook.Chapter_03
+import FormalBook.Chapter_04
+import FormalBook.Chapter_05
+import FormalBook.Chapter_06
+import FormalBook.Chapter_07
+import FormalBook.Chapter_08
+import FormalBook.Chapter_09
+import FormalBook.Chapter_10
+import FormalBook.Chapter_11
+import FormalBook.Chapter_12
+import FormalBook.Chapter_13
+import FormalBook.Chapter_14
+import FormalBook.Chapter_15
+import FormalBook.Chapter_16
+import FormalBook.Chapter_17
+import FormalBook.Chapter_18
+import FormalBook.Chapter_19
+import FormalBook.Chapter_20
+import FormalBook.Chapter_21
+import FormalBook.Chapter_22
+import FormalBook.Chapter_23
+import FormalBook.Chapter_24
+import FormalBook.Chapter_25
+import FormalBook.Chapter_26
+import FormalBook.Chapter_27
+import FormalBook.Chapter_28
+import FormalBook.Chapter_29
+import FormalBook.Chapter_30
+import FormalBook.Chapter_31
+import FormalBook.Chapter_33
+import FormalBook.Chapter_32
+import FormalBook.Chapter_34
+import FormalBook.Chapter_35
+import FormalBook.Chapter_36
+import FormalBook.Chapter_37
+import FormalBook.Chapter_38
+import FormalBook.Chapter_39
+import FormalBook.Chapter_40
+import FormalBook.Chapter_41
+import FormalBook.Chapter_42
+import FormalBook.Chapter_43
+import FormalBook.Chapter_44
+import FormalBook.Chapter_45

FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean FormalBook/Chapter_01.lean

@@ -133,11 +133,9 @@ lemma ZMod.two_ne_one (q : ℕ)  [Fact (1 < q)] : (2 : ZMod q) ≠ 1 := by
   intro h1
   have h : (2 - 1 : ZMod q) = 0 := by exact Iff.mpr sub_eq_zero h1
   norm_num at h
-#check pred_le_pred
 
 lemma sub_one_le_sub_one {n m : ℕ} : n ≤ m → n - 1 ≤ m - 1 := by
-  intro h
-  exact pred_le_pred h
+  exact fun h => pred_le_pred h
 
 
 theorem infinity_of_primes₃: