Merge branch 'mo271:main' into main

.github/workflows/blueprint.yml

@@ -0,0 +1,92 @@
+on:
+  push:
+    branches:
+      - main
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
+
+      - name: Update checkdecls
+        run: ~/.elan/bin/lake update checkdecls
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build FormalBook
+
+      - name: Cache mathlib docs
+        uses: actions/cache@v3
+        with:
+          path: |
+            .lake/build/doc/Init
+            .lake/build/doc/Lake
+            .lake/build/doc/Lean
+            .lake/build/doc/Std
+            .lake/build/doc/Mathlib
+            .lake/build/doc/declarations
+            !.lake/build/doc/declarations/declaration-data-FormalBook*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build FormalBook:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install git+https://github.com/PatrickMassot/leanblueprint.git@client
+            leanblueprint pdf
+            mkdir docs
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      - name: Check declarations
+        run: |
+            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Move documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs
+
+      - name: Upload docs & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: |
+          mv docs/docs .lake/build/doc

FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean

@@ -15,23 +15,9 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Mathlib.Analysis.Asymptotics.Asymptotics
-import Mathlib.Tactic
-import Mathlib.Data.Nat.Prime
-import Mathlib.Data.Nat.Pow
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Data.Nat.Parity
-import Mathlib.FieldTheory.Finite.Basic
-import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.GroupTheory.Coset
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.PrimeCounting
-import Mathlib.Order.Filter.AtTopBot
-import Mathlib.Topology.Instances.ENNReal
-import Mathlib.Topology.Basic
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 open Finset Nat
 open BigOperators
@@ -146,8 +132,6 @@ 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
-  have := ZMod.one_ne_zero q
-  exact this h
 
 
 theorem infinity_of_primes₃:

FormalBook/Ch02_Bertrand's_postulate.lean

@@ -125,7 +125,7 @@ theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n)
   apply Finset.prod_subset
   · exact Finset.range_subset.2 (add_le_add_right (Nat.div_le_self _ _) _)
   intro x hx h2x
-  rw [Finset.mem_range, lt_succ_iff] at hx h2x
+  rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
   rw [not_le, div_lt_iff_lt_mul' three_pos, mul_comm x] at h2x
   replace no_prime := not_exists.mp no_prime x
   rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime
@@ -150,7 +150,8 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n)
   let f x := x ^ n.centralBinom.factorization x
   have : ∏ x : ℕ in S, f x = ∏ x : ℕ in Finset.range (2 * n / 3 + 1), f x := by
     refine' Finset.prod_filter_of_ne fun p _ h => _
-    contrapose! h; dsimp only
+    contrapose! h
+    dsimp [f]
     rw [factorization_eq_zero_of_non_prime n.centralBinom h, _root_.pow_zero]
   rw [centralBinom_factorization_small n n_big no_prime, ← this, ←
     Finset.prod_filter_mul_prod_filter_not S (· ≤ Nat.sqrt (2 * n))]

FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean

@@ -15,12 +15,8 @@ limitations under the License.
 
 Authors: Moritz Firsching, Nikolas Kuhn
 -/
-import Mathlib.Tactic
+import Mathlib.Algebra.Polynomial.Basic
 import Mathlib.Data.ZMod.Basic
-import Mathlib.Data.Finset.Card
-import Mathlib.Data.Polynomial.Basic
-import Mathlib.Order.LocallyFinite
-
 
 open ZMod Finset
 open Polynomial (X)

FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean

@@ -15,20 +15,10 @@ limitations under the License.
 
 Authors: Moritz Firsching, Nick Kuhn
 -/
-import Mathlib.Tactic
-import Mathlib.Data.Set.Basic
-import Mathlib.Data.Fintype.Card
-import Mathlib.RingTheory.IntegralDomain
-import Mathlib.RingTheory.Subring.Basic
-import Mathlib.RingTheory.RootsOfUnity.Complex
-import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
-import Mathlib.Data.Polynomial.RingDivision
-import Mathlib.Algebra.Group.Conj
-import Mathlib.LinearAlgebra.FiniteDimensional
-import Mathlib.LinearAlgebra.Basis
-import Mathlib.Data.Polynomial.Basic
-import Mathlib.Data.Complex.Basic
-import Mathlib.GroupTheory.ClassEquation
+import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.HopfAlgebra
+import Mathlib.RingTheory.LittleWedderburn
+import Mathlib.Algebra.Lie.OfAssociative
 
 open Finset Subring Polynomial Complex BigOperators Nat
 /-!
@@ -112,8 +102,9 @@ theorem h_lamb_gt_q_sub_one (q n : ℕ) (lamb : ℂ):
   have g := (Real.sqrt_lt_sqrt_iff this).mpr (h_ineq)
   have : Real.sqrt (((q:ℝ) - 1) ^ 2) = ((q : ℝ) - 1) := by sorry
   rw [this] at g
-  simp only [norm_eq_abs, map_nonneg, Real.sqrt_sq] at g
-  exact g
+  rw [norm_eq_abs, Real.sqrt_sq] at g
+  · exact g
+  · aesop
 
 lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
     (H : q ^ k - 1 ∣ q ^ n - 1) : k ∣ n := by
@@ -131,14 +122,14 @@ lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
         calc
           _ < q := hq
           _ = q^1 := (Nat.pow_one q).symm
-          _ ≤ q ^ m := (pow_le_pow_iff hq).mpr hm
+          _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
       exact Nat.sub_pos_of_lt this
     have : q ^ k - 1 ≤ q ^ m - 1 := Nat.le_of_dvd this H
     have :  q ^ k ≤ q ^ m  := by
       zify at this
       simp at this
       simpa [Nat.sub_add_cancel <| one_le_pow m q hq'] using this
-    exact (pow_le_pow_iff hq).mp this
+    exact (pow_le_pow_iff_right hq).mp this
 
   have : q ^ m - 1 = q^(m - k)*(q ^ k - 1) + (q^(m - k) - 1) := by
     zify
@@ -310,10 +301,8 @@ theorem wedderburn (h: Fintype R): IsField R := by
       intro hs
       apply(Int.dvd_div_of_mul_dvd _)
       have h_one_neq: 1 ≠ n_k A := by
-        dsimp only
         sorry
       have h_k_n_lt_n: n_k A < n := by
-        dsimp only
         sorry
       have h_noneval := phi_div_2 n (n_k A) h_one_neq (h_n_k_A_dvd A) h_k_n_lt_n
       have := @eval_dvd ℤ _ _ _ q h_noneval
@@ -330,14 +319,15 @@ theorem wedderburn (h: Fintype R): IsField R := by
       rw [cast_add] at this
       rw [← this]
       simp [hq_pow_pos n]
-    simp [hq] at h1'
+    --rw [hq] at h1'
+    norm_num at h1'
     simp [h1'] at h₁_dvd
-    rw [← hq] at h₁_dvd
-    exact (Int.dvd_add_left h₂_dvd).mp h₁_dvd
+    refine (Int.dvd_add_left h₂_dvd).mp ?_
+    convert h₁_dvd
 
   by_contra
 
-  have g : map (Int.castRingHom ℂ) (phi n) = ∏ lamb in (primitiveRoots n ℂ), (X - C lamb) := by
+  have g : Polynomial.map (Int.castRingHom ℂ) (phi n) = ∏ lamb in (primitiveRoots n ℂ), (X - C lamb) := by
     dsimp only [phi]
     simp only [map_cyclotomic]
     have := isPrimitiveRoot_exp n h_n
@@ -378,10 +368,10 @@ theorem wedderburn (h: Fintype R): IsField R := by
 
   refine' not_le_of_gt h_gt _
   have : (q - 1 : ℕ) = (q : ℤ) - 1 := by
-    exact Int.coe_pred_of_pos this
+    exact Int.natCast_pred_of_pos this
   rw [← this] at h_norm
   have : Int.natAbs (eval (↑q) (cyclotomic n ℤ)) = |eval (↑q) (phi n)| := by
-    simp only [Int.coe_natAbs]
+    simp only [Int.natCast_natAbs]
     rfl
   rw [← this] at h_norm
   exact_mod_cast h_norm

FormalBook/Ch44_Of_friends_and_politicians.lean

@@ -85,7 +85,7 @@ theorem friendship_theorem [Nonempty V]
           refine' Fintype.one_lt_card_iff.mpr _
           use v
           use x
-        rw [eq₁] at this
+        rw [(show Fintype.card V = n by rfl), eq₁] at this
         tauto
     -- In case k = 2, we have G = K₃
     · norm_num at eq₁
@@ -104,7 +104,7 @@ theorem friendship_theorem [Nonempty V]
           exact fun h => ⟨(G.ne_of_adj h).symm, Finset.mem_univ _⟩
         convert_to 2 ≤ _
         · convert_to _ = Fintype.card V - 1
-          · rw [eq₁]
+          · rw [(show Fintype.card V = n by rfl), eq₁]
           · exact Finset.card_erase_of_mem (Finset.mem_univ _)
         · rw [hregular]
       rw [this]