Skip to content

Commit 0420755

Browse files
mo271mo271
committed
bump mathlib
1 parent 223d142 commit 0420755

4 files changed

Lines changed: 101 additions & 101 deletions

File tree

‎FormalBook/Chapter_01.lean‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,11 @@ Copyright 2022 Moritz Firsching. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Moritz Firsching, Ralf Stephan
55
-/
6+
import Mathlib.Algebra.Order.Ring.Star
7+
import Mathlib.Data.Int.Lemmas
8+
import Mathlib.Data.Int.Star
69
import Mathlib.NumberTheory.LucasLehmer
710
import Mathlib.NumberTheory.PrimeCounting
8-
import Mathlib.NumberTheory.Fermat
9-
import Mathlib.Analysis.SpecialFunctions.Pow.Real
1011

1112
open Finset Nat
1213
open BigOperators
@@ -27,7 +28,7 @@ open BigOperators
2728
-/
2829
theorem infinity_of_primes₁ (S : Finset ℕ) (h : ∀ q ∈ S, Nat.Prime q):
2930
∃ (p : ℕ), Nat.Prime p ∧ p ∉ S := by
30-
let n := 1 + ∏ q in S, q
31+
let n := 1 + ∏ q ∈ S, q
3132
/- "This `n` has a prime divisor":
3233
we pick the minimal one, the argument works with any prime divisor -/
3334
let p := n.minFac
@@ -36,8 +37,8 @@ theorem infinity_of_primes₁ (S : Finset ℕ) (h : ∀ q ∈ S, Nat.Prime q):
3637
(Finset.prod_pos fun q hq ↦ Prime.pos <| h q hq)
3738
refine ⟨hp, ?_⟩
3839
by_contra a
39-
have h_p_div_prod : p ∣ ∏ q in S, q := dvd_prod_of_mem (fun (i : ℕ) ↦ i) a
40-
have h_p_div_diff : p ∣ n - ∏ q in S, q := dvd_sub' (minFac_dvd n) h_p_div_prod
40+
have h_p_div_prod : p ∣ ∏ q ∈ S, q := dvd_prod_of_mem (fun (i : ℕ) ↦ i) a
41+
have h_p_div_diff : p ∣ n - ∏ q ∈ S, q := dvd_sub (minFac_dvd n) h_p_div_prod
4142
have h_p_div_one : p ∣ 1 := by aesop
4243
exact Nat.Prime.not_dvd_one hp h_p_div_one
4344

@@ -52,7 +53,7 @@ local notation "F" => fermatNumber
5253
-- We actually prove something slighly stronger that what is in the book:
5354
-- also for n = 0, the statement is true.
5455
-- This is in mathlib as `fermatNumber_product`
55-
lemma fermatProduct (n : ℕ) : ∏ k in range n, F k = F n - 2 := by
56+
lemma fermatProduct (n : ℕ) : ∏ k ∈ range n, F k = F n - 2 := by
5657
induction' n with n hn
5758
· trivial
5859
· rw [prod_range_succ, hn]
@@ -67,9 +68,9 @@ theorem infinity_of_primes₂ (k n : ℕ) (h : k < n) : Coprime (F n) (F k) :=
6768
have h_n : m ∣ F n := (F n).gcd_dvd_left (F k)
6869
have h_k : m ∣ F k := (F n).gcd_dvd_right (F k)
6970
have h_m : m ∣ 2 := by
70-
have h_m_prod : m ∣ (∏ k in range n, F k) :=
71+
have h_m_prod : m ∣ (∏ k ∈ range n, F k) :=
7172
dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
72-
have h_prod : (∏ k in range n, F k) + 2 = F n := by
73+
have h_prod : (∏ k ∈ range n, F k) + 2 = F n := by
7374
rw [fermatProduct, Nat.sub_add_cancel]
7475
refine' le_of_lt _
7576
simp [two_lt_fermatNumber]
@@ -116,8 +117,7 @@ theorem infinity_of_primes₃:
116117
rw [modEq_iff_dvd, dvd_iff_exists_eq_mul_left] at *
117118
obtain ⟨c, hc⟩ := this
118119
use c
119-
simp only [CharP.cast_eq_zero, ge_iff_le, gt_iff_lt, pow_pos, cast_pred, cast_pow, cast_ofNat,
120-
zero_sub, neg_sub] at hc
120+
simp only [CharP.cast_eq_zero, zero_sub] at hc
121121
simp [cast_one, cast_pow, cast_ofNat, hc.symm]
122122
have h_mod_q' : (2 : (ZMod q)) ^ p = 1 := by
123123
have := (ZMod.natCast_eq_natCast_iff _ _ _).mpr h_mod_q
@@ -154,9 +154,9 @@ theorem infinity_of_primes₃:
154154
exact (totient_prime hq).symm
155155
refine ⟨q, minFac_prime <| Nat.ne_of_gt ?_, ?_⟩
156156
· calc 1 < 2^2 - 1 := one_lt_succ_succ 1
157-
_ ≤ 2^p - 1 := sub_one_le_sub_one <| pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
157+
_ ≤ 2^p - 1 := sub_one_le_sub_one <| Nat.pow_le_pow_right (succ_pos 1) (Prime.two_le hp)
158158
· have h2q : 2 ≤ q := Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
159-
Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1
159+
Nat.sub_le_sub_right ((Nat.pow_le_pow_right (succ_pos 1) (Prime.two_le hp))) 1
160160
exact lt_of_le_of_lt (Nat.le_of_dvd (Nat.sub_pos_of_lt <| h2q) h_piv_div_q_sub_one)
161161
<| pred_lt <| Nat.ne_of_gt <| Nat.le_of_lt h2q
162162

@@ -181,11 +181,11 @@ theorem infinity_of_primes₄ : Tendsto π atTop atTop := by
181181
have H_log_le_primeCountingReal_add_one (n : ℕ) (x : ℝ) (hxge : x ≥ n) (hxlt : x < n + 1) :
182182
Real.log x ≤ primeCountingReal x + 1 :=
183183
calc
184-
Real.log x ≤ ∑ k in Icc 1 n, (k : ℝ)⁻¹ := by sorry
184+
Real.log x ≤ ∑ k ∈ Icc 1 n, (k : ℝ)⁻¹ := by sorry
185185
_ ≤ (∑' m : (S₁ x), (m : ℝ)⁻¹) := by sorry
186-
_ ≤ (∏ p in primesBelow ⌊x⌋.natAbs, (∑' k : ℕ, (p ^ k : ℝ)⁻¹)) := by sorry
187-
_ ≤ (∏ k in Icc 1 (primeCountingReal x), (nth Nat.Prime k) / ((nth Nat.Prime k) - 1)) := by sorry
188-
_ ≤ (∏ k in Icc 1 (primeCountingReal x), (k + 1) / k) := by sorry
186+
_ ≤ (∏ p ∈ primesBelow ⌊x⌋.natAbs, (∑' k : ℕ, (p ^ k : ℝ)⁻¹)) := by sorry
187+
_ ≤ (∏ k ∈ Icc 1 (primeCountingReal x), (nth Nat.Prime k) / ((nth Nat.Prime k) - 1)) := by sorry
188+
_ ≤ (∏ k ∈ Icc 1 (primeCountingReal x), (k + 1) / k) := by sorry
189189
_ ≤ primeCountingReal x + 1 := by sorry
190190
sorry
191191

@@ -212,23 +212,23 @@ lemma H_P4_1 {k p: ℝ} (hk: k > 0) (hp: p ≥ k + 1): p / (p - 1) ≤ (k + 1) /
212212
@le_sub_iff_add_le]
213213
exact hp
214214

215-
lemma prod_Icc_succ_div (n : ℕ) (hn : 2 ≤ n) : (∏ x in Icc 1 n, ((x + 1) : ℝ) / x) = n + 1 := by
216-
rw [← Nat.Ico_succ_right]
215+
lemma prod_Icc_succ_div (n : ℕ) (hn : 2 ≤ n) : (∏ x ∈ Icc 1 n, ((x + 1) : ℝ) / x) = n + 1 := by
216+
rw [← Finset.Ico_succ_right_eq_Icc]
217217
induction' n with n h
218218
· simp
219-
· rw [Finset.prod_Ico_succ_top <| Nat.le_add_left 1 n]
220-
norm_num
219+
· simp only [succ_eq_succ, succ_eq_add_one] at h ⊢
220+
rw [Finset.prod_Ico_succ_top <| Nat.le_add_left 1 n]
221221
cases' lt_or_ge n 2 with _ h2
222222
· interval_cases n
223223
· tauto
224224
· norm_num
225225
field_simp [Finset.prod_eq_zero_iff] at h ⊢
226226
rw [h h2]
227-
ring
227+
norm_num
228228

229229
-- Removed unnecessary assumption `(hpi3 : (π 3) = 2)`
230230
lemma H_P4_2 (x : ℕ) (hx : x ≥ 3) :
231-
(∏ x in Icc 1 (π x), ((x + 1) : ℝ) / x) = (π x) + 1 := by
231+
(∏ x ∈ Icc 1 (π x), ((x + 1) : ℝ) / x) = (π x) + 1 := by
232232
rw [prod_Icc_succ_div]
233233
exact Monotone.imp monotone_primeCounting hx
234234

@@ -334,7 +334,7 @@ using the sum of inverses of primes
334334
-/
335335
-- see Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
336336
theorem infinity_of_primes₆ :
337-
Tendsto (fun n ↦ ∑ p in Finset.filter (fun p ↦ Nat.Prime p) (range n), 1 / (p : ℝ))
337+
Tendsto (fun n ↦ ∑ p ∈ Finset.filter (fun p ↦ Nat.Prime p) (range n), 1 / (p : ℝ))
338338
atTop atTop := by
339339
sorry
340340

‎FormalBook/Chapter_06.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Moritz Firsching, Nick Kuhn
55
-/
66
import Mathlib.RingTheory.Henselian
7-
import Mathlib.RingTheory.HopfAlgebra
7+
import Mathlib.RingTheory.HopfAlgebra.Basic
88
import Mathlib.RingTheory.LittleWedderburn
99
import Mathlib.Algebra.Lie.OfAssociative
1010

‎lake-manifest.json‎

Lines changed: 76 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -1,62 +1,82 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover-community/batteries",
4+
[{"url": "https://github.com/leanprover/doc-gen4",
55
"type": "git",
66
"subDir": null,
7-
"scope": "leanprover-community",
8-
"rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
9-
"name": "batteries",
7+
"scope": "",
8+
"rev": "3721ccdc8ce7c515cd60d385e5d5a463d6bf0383",
9+
"name": "«doc-gen4»",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
12-
"inherited": true,
13-
"configFile": "lakefile.toml"},
14-
{"url": "https://github.com/leanprover-community/quote4",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/PatrickMassot/checkdecls.git",
1515
"type": "git",
1616
"subDir": null,
17-
"scope": "leanprover-community",
18-
"rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
19-
"name": "Qq",
17+
"scope": "",
18+
"rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
19+
"name": "checkdecls",
2020
"manifestFile": "lake-manifest.json",
21-
"inputRev": "master",
22-
"inherited": true,
21+
"inputRev": null,
22+
"inherited": false,
2323
"configFile": "lakefile.lean"},
24-
{"url": "https://github.com/leanprover-community/aesop",
24+
{"url": "https://github.com/leanprover-community/mathlib4.git",
2525
"type": "git",
2626
"subDir": null,
27-
"scope": "leanprover-community",
28-
"rev": "de91b59101763419997026c35a41432ac8691f15",
29-
"name": "aesop",
27+
"scope": "",
28+
"rev": "4aa8d324e47fd06e39e5a0985653f79979fd1308",
29+
"name": "mathlib",
3030
"manifestFile": "lake-manifest.json",
31-
"inputRev": "master",
31+
"inputRev": null,
32+
"inherited": false,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/mhuisi/lean4-cli",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "6667b921594697980586296511fab6a359e802d1",
39+
"name": "Cli",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
3242
"inherited": true,
3343
"configFile": "lakefile.toml"},
34-
{"url": "https://github.com/leanprover-community/ProofWidgets4",
44+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
3545
"type": "git",
3646
"subDir": null,
37-
"scope": "leanprover-community",
38-
"rev": "1383e72b40dd62a566896a6e348ffe868801b172",
39-
"name": "proofwidgets",
47+
"scope": "",
48+
"rev": "d3195374a885cf2b0bfa66063deb493686029f95",
49+
"name": "UnicodeBasic",
4050
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.46",
51+
"inputRev": "main",
4252
"inherited": true,
4353
"configFile": "lakefile.lean"},
44-
{"url": "https://github.com/leanprover/lean4-cli",
54+
{"url": "https://github.com/dupuisf/BibtexQuery",
4555
"type": "git",
4656
"subDir": null,
47-
"scope": "leanprover",
48-
"rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
49-
"name": "Cli",
57+
"scope": "",
58+
"rev": "1b05159ad44f220cec7489e65e6bc4b1e178b67f",
59+
"name": "BibtexQuery",
5060
"manifestFile": "lake-manifest.json",
51-
"inputRev": "main",
61+
"inputRev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
5262
"inherited": true,
5363
"configFile": "lakefile.toml"},
54-
{"url": "https://github.com/leanprover-community/import-graph",
64+
{"url": "https://github.com/acmepjz/md4lean",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "",
68+
"rev": "feac4e0c356b0928657bf3b54fa83ae952f53257",
69+
"name": "MD4Lean",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "main",
72+
"inherited": true,
73+
"configFile": "lakefile.lean"},
74+
{"url": "https://github.com/leanprover-community/plausible",
5575
"type": "git",
5676
"subDir": null,
5777
"scope": "leanprover-community",
58-
"rev": "119b022b3ea88ec810a677888528e50f8144a26e",
59-
"name": "importGraph",
78+
"rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
79+
"name": "plausible",
6080
"manifestFile": "lake-manifest.json",
6181
"inputRev": "main",
6282
"inherited": true,
@@ -65,81 +85,61 @@
6585
"type": "git",
6686
"subDir": null,
6787
"scope": "leanprover-community",
68-
"rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
88+
"rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
6989
"name": "LeanSearchClient",
7090
"manifestFile": "lake-manifest.json",
7191
"inputRev": "main",
7292
"inherited": true,
7393
"configFile": "lakefile.toml"},
74-
{"url": "https://github.com/leanprover-community/plausible",
94+
{"url": "https://github.com/leanprover-community/import-graph",
7595
"type": "git",
7696
"subDir": null,
7797
"scope": "leanprover-community",
78-
"rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
79-
"name": "plausible",
98+
"rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
99+
"name": "importGraph",
80100
"manifestFile": "lake-manifest.json",
81101
"inputRev": "main",
82102
"inherited": true,
83103
"configFile": "lakefile.toml"},
84-
{"url": "https://github.com/leanprover-community/mathlib4.git",
85-
"type": "git",
86-
"subDir": null,
87-
"scope": "",
88-
"rev": "0e836d6e1a3c5ed008688622e261e19fbef05e0e",
89-
"name": "mathlib",
90-
"manifestFile": "lake-manifest.json",
91-
"inputRev": null,
92-
"inherited": false,
93-
"configFile": "lakefile.lean"},
94-
{"url": "https://github.com/PatrickMassot/checkdecls.git",
95-
"type": "git",
96-
"subDir": null,
97-
"scope": "",
98-
"rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
99-
"name": "checkdecls",
100-
"manifestFile": "lake-manifest.json",
101-
"inputRev": null,
102-
"inherited": false,
103-
"configFile": "lakefile.lean"},
104-
{"url": "https://github.com/acmepjz/md4lean",
104+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
105105
"type": "git",
106106
"subDir": null,
107-
"scope": "",
108-
"rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
109-
"name": "MD4Lean",
107+
"scope": "leanprover-community",
108+
"rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
109+
"name": "proofwidgets",
110110
"manifestFile": "lake-manifest.json",
111-
"inputRev": "main",
111+
"inputRev": "v0.0.71",
112112
"inherited": true,
113113
"configFile": "lakefile.lean"},
114-
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
114+
{"url": "https://github.com/leanprover-community/aesop",
115115
"type": "git",
116116
"subDir": null,
117-
"scope": "",
118-
"rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
119-
"name": "UnicodeBasic",
117+
"scope": "leanprover-community",
118+
"rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
119+
"name": "aesop",
120120
"manifestFile": "lake-manifest.json",
121-
"inputRev": "main",
121+
"inputRev": "master",
122122
"inherited": true,
123-
"configFile": "lakefile.lean"},
124-
{"url": "https://github.com/dupuisf/BibtexQuery",
123+
"configFile": "lakefile.toml"},
124+
{"url": "https://github.com/leanprover-community/quote4",
125125
"type": "git",
126126
"subDir": null,
127-
"scope": "",
128-
"rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
129-
"name": "BibtexQuery",
127+
"scope": "leanprover-community",
128+
"rev": "f85ad59c9b60647ef736719c23edd4578f723806",
129+
"name": "Qq",
130130
"manifestFile": "lake-manifest.json",
131131
"inputRev": "master",
132132
"inherited": true,
133-
"configFile": "lakefile.lean"},
134-
{"url": "https://github.com/leanprover/doc-gen4",
133+
"configFile": "lakefile.toml"},
134+
{"url": "https://github.com/leanprover-community/batteries",
135135
"type": "git",
136136
"subDir": null,
137-
"scope": "",
138-
"rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
139-
"name": "«doc-gen4»",
137+
"scope": "leanprover-community",
138+
"rev": "76408f09466811154e0e42329962de19f95d178b",
139+
"name": "batteries",
140140
"manifestFile": "lake-manifest.json",
141141
"inputRev": "main",
142-
"inherited": false,
143-
"configFile": "lakefile.lean"}],
142+
"inherited": true,
143+
"configFile": "lakefile.toml"}],
144144
"name": "FormalBook",
145145
"lakeDir": ".lake"}

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.14.0-rc2
1+
leanprover/lean4:v4.23.0-rc2

0 commit comments

Comments
 (0)