Merge branch 'master' into pointwise-ergodic-thm

Author: oliver-butterley

Archive.lean

@@ -74,7 +74,6 @@ import Archive.Wiedijk100Theorems.FriendshipGraphs
 import Archive.Wiedijk100Theorems.HeronsFormula
 import Archive.Wiedijk100Theorems.InverseTriangleSum
 import Archive.Wiedijk100Theorems.Konigsberg
-import Archive.Wiedijk100Theorems.Partition
 import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubicQuartic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges

Archive/Examples/Kuratowski.lean

@@ -22,7 +22,7 @@ complements of the closed sets, and `s` and `sᶜ` which are neither closed nor
 This reduces `14*13/2 = 91` inequalities to check down to `6*5/2 = 15` inequalities.
 We'll further show that the 15 inequalities follow from a subset of 6 by algebra.
 
-There are charaterizations and criteria for a set to be a 14-set in the paper
+There are characterizations and criteria for a set to be a 14-set in the paper
 "Characterization of Kuratowski 14-Sets" by Eric Langford which we do not formalize.
 
 ## Main definitions
@@ -63,7 +63,7 @@ theorem sum_map_theClosedSix_add_compl (s : Set X) :
     ((theClosedSix s).map fun t ↦ {t} + {tᶜ}).sum = theClosedSix s + theOpenSix s :=
   Multiset.sum_map_add
 
-/-- `theFourteen s` can be splitted into 3 subsets. -/
+/-- `theFourteen s` can be split into 3 subsets. -/
 theorem theFourteen_eq_pair_add_theClosedSix_add_theOpenSix (s : Set X) :
     theFourteen s = {s, sᶜ} + theClosedSix s + theOpenSix s := by
   rw [add_assoc, ← sum_map_theClosedSix_add_compl]; rfl

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -143,7 +143,7 @@ theorem real_roots_Phi_ge (hab : b < a) : 2 ≤ Fintype.card ((Φ ℚ a b).rootS
     Finset.card_insert_of_notMem (mt Finset.mem_singleton.mp hxy)]
 
 theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a b).rootSet ℂ) = 5 :=
-  (card_rootSet_eq_natDegree h (IsAlgClosed.splits_codomain _)).trans (natDegree_Phi a b)
+  (card_rootSet_eq_natDegree h (IsAlgClosed.splits _)).trans (natDegree_Phi a b)
 
 theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) :
     Bijective (galActionHom (Φ ℚ a b) ℂ) := by

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -218,7 +218,7 @@ theorem first_vote_pos :
         count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
         Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
       · norm_cast
-        rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
+        rw [mul_comm _ (p + 1), add_right_comm, Nat.add_one_mul_choose_eq,
           mul_comm]
       all_goals simp [(Nat.choose_pos <| le_add_of_nonneg_right zero_le').ne']
     · simp