Merge branch 'main' into golf-proofs

Author: pitmonticone

FLT/Basic/Reductions.lean

@@ -1,5 +1,6 @@
 import Mathlib.Data.PNat.Basic
 import Mathlib.NumberTheory.FLT.Four
+import Mathlib.NumberTheory.FLT.Three
 import Mathlib.Tactic
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
 import Mathlib.RepresentationTheory.Basic
@@ -49,12 +50,6 @@ theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem :
   specialize h₁ n h₂ a b c (by simp) (by simp) (by simp)
   assumption_mod_cast
 
-/-- Fermat's Last Theorem is true when n = 3. -/
-lemma fermatLastTheoremThree : FermatLastTheoremFor 3 := sorry
--- This is proved in the FLT-regular project (https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698)
--- and the FLT3 project (https://github.com/riccardobrasca/flt3).
--- The way to turn this node green is to port this latter one to mathlib so we can use it here.
-
 namespace FLT
 
 /-- If Fermat's Last Theorem is true for primes `p ≥ 5`, then FLT is true. -/

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -11,7 +11,7 @@ import Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
 import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 import Mathlib.LinearAlgebra.UnitaryGroup
-import Mathlib.RepresentationTheory.FdRep
+import Mathlib.RepresentationTheory.FDRep
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Topology.LocallyConstant.Basic
 
@@ -278,7 +278,7 @@ structure preweight (n : ℕ) where
 open CategoryTheory
 
 noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
-    FdRep ℂ (orthogonalGroup (Fin n) ℝ) where
+    FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
   V := FGModuleCat.of ℂ (Fin w.d → ℂ)
   ρ := {
     toFun := fun A ↦ {

blueprint/src/chapter/ch02reductions.tex

@@ -28,10 +28,10 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
   There are no solutions in positive integers to $a^3+b^3=c^3$.
 \end{lemma}
 \begin{proof}
+  \leanok
   A proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\underline{here}}.
   Another proof has been formalised in Lean in the FLT3 project \href{https://github.com/riccardobrasca/flt3}{\underline{here}} by a team from the Lean For the Curious Mathematician conference held in Luminy in March 2024
   (its dependency graph can be visualised \href{https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html}{\underline{here}}).
-  To get this node green, this latter proof needs to be upstreamed to mathlib. This is currently work in progress by the same team.
 \end{proof}
 
 \begin{corollary}\label{FLT.of_p_ge_5}\lean{FLT.of_p_ge_5}\leanok If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$ with $p$ prime and $p\geq 5$.

blueprint/src/chapter/ch07exampleGLn.tex

@@ -142,7 +142,7 @@ \section{Automorphic forms}
   \label{AutomorphicForm.GLn.AutomorphicFormForGLnOverQ}
   \lean{AutomorphicForm.GLn.AutomorphicFormForGLnOverQ}
   \uses{AutomorphicForm.GLn.IsSmooth, AutomorphicForm.GLn.IsSlowlyIncreasing,
-    AutomorphicForm.GLn.weight, instCentreAction}
+    AutomorphicForm.GLn.Weight, instCentreAction}
   A smooth function $f:\GL_n(\A_{\Q}^f)\times\GL_n(\R)\to\bbC$ is
   an $O_n(\R)$-\emph{automorphic form} on $\GL_n(\A_{\Q})$ if it satisfies the following
   five conditions.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc4a6b1ac3cd502988e283d5c9c5fdf261125a07",
+   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "363b8176ac29271af4b000b649f836c846f528fc",
+   "rev": "90ef20a210ecd605e8036b280b6b85b9043b5447",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,17 +95,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
+   "rev": "f93115d0209de6db335725dee900d379f40c0317",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b5197b656018a2d929e025f41aca5ba463557dd1",
+   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc1
+leanprover/lean4:v4.10.0-rc2