Build the entire project

Author: Ruben-VandeVelde

FLT/FLT_files.lean

@@ -1,9 +1,28 @@
+import FLT.AutomorphicForm.QuaternionAlgebra
+import FLT.AutomorphicRepresentation.Example
 import FLT.Basic.Reductions
 import FLT.EllipticCurve.Torsion
+import FLT.ForMathlib.ActionTopology
+import FLT.ForMathlib.FGModuleTopology
+import FLT.ForMathlib.MiscLemmas
+import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
+import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.ContinuousSMul_topology
+import FLT.HIMExperiments.dual_topology
+import FLT.HIMExperiments.flatness
+import FLT.HIMExperiments.module_topology
+import FLT.HIMExperiments.right_module_topology
 import FLT.Hard.Results
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.Frobenius
+import FLT.MathlibExperiments.Frobenius2
+import FLT.MathlibExperiments.FrobeniusRiou
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
 import FLT.TateCurve.TateCurve
-import FLT.AutomorphicRepresentation.Example
-import FLT.mathlibExperiments.IsCentralSimple

FLT/ForMathlib/FGModuleTopology.lean

@@ -1,4 +1,5 @@
 import Mathlib.Algebra.Module.Projective
+import Mathlib.Data.Finite.Card
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.Topology.Algebra.Module.Basic
 import FLT.ForMathlib.MiscLemmas
@@ -31,8 +32,6 @@ or $p$-adics).
 
 -/
 
-set_option lang.lemmaCmd true
-
 section basics
 
 variable (R : Type*) [TopologicalSpace R] [Semiring R]

FLT/HIMExperiments/ContinuousSMul_topology.lean

@@ -80,6 +80,9 @@ functions from `A` (now considered only as an index set, so with no topology) to
 
 -/
 
+-- See FLT.ForMathlib.ActionTopology for a parallel development.
+#exit
+
 section continuous_smul
 
 variable {R : Type} [τR : TopologicalSpace R]

FLT/HIMExperiments/dual_topology.lean

@@ -90,6 +90,9 @@ functions from `A` (now considered only as an index set, so with no topology) to
 
 -/
 
+-- See FLT.ForMathlib.ActionTopology for a parallel development.
+#exit
+
 section basics
 
 variable (R : Type*) [Monoid R] [TopologicalSpace R] [ContinuousMul R]

FLT/HIMExperiments/right_module_topology.lean

@@ -35,6 +35,9 @@ functions from `M` (now considered only as an index set, so with no topology) to
 
 -/
 
+-- See FLT.ForMathlib.ActionTopology for a parallel development.
+#exit
+
 section defs
 
 class IsActionTopology (R M : Type*) [SMul R M]

FLT/MathlibExperiments/Coalgebra/Monoid.lean

@@ -5,7 +5,7 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 -/
 
 import Mathlib.RingTheory.TensorProduct.Basic
-import FLT.mathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.Sweedler
 import Mathlib.RingTheory.HopfAlgebra
 
 /-!

FLT/MathlibExperiments/Coalgebra/TensorProduct.lean

@@ -6,7 +6,7 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 
 import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.Bialgebra.Basic
-import FLT.mathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.Sweedler
 
 /-!
 

FLT/MathlibExperiments/HopfAlgebra/Basic.lean

@@ -5,8 +5,8 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 -/
 
 import Mathlib.RingTheory.HopfAlgebra
-import FLT.mathlibExperiments.Coalgebra.Monoid
-import FLT.mathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
 import Mathlib.Tactic.Group
 
 /-!
@@ -16,7 +16,7 @@ For an `R`-hopf algebra `A`, we prove in this file the following basic propertie
 - the antipodal map is anticommutative;
 - the antipodal map is unique linear map whose convolution inverse is the identity `𝟙 A`.
   (Note that, confusingly, the identity linear map `x ↦ x` is not actually the unit in the monoid
-  structure of linear maps. See `mathlibExperiments/Coalgebra/Monoid.lean`)
+  structure of linear maps. See `MathlibExperiments/Coalgebra/Monoid.lean`)
 if we further assume `A` is commutative then
 - the `R`-algebra homomorphisms from `A` to `L` has a group structure where multiplication is
   convolution, and inverse of `f `is `f ∘ antipode`