Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

Author: kbuzzard

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -144,13 +144,16 @@ def smul (r : R) (φ : AutomorphicForm F D R W U χ) :
 instance : SMul R (AutomorphicForm F D R W U χ) where
   smul := smul
 
+lemma smul_apply (r : R) (φ : AutomorphicForm F D R W U χ) (g : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
+    (r • φ) g = r • (φ g) := rfl
+
 instance module : Module R (AutomorphicForm F D R W U χ) where
-  one_smul := sorry
-  mul_smul := sorry
-  smul_zero := sorry
-  smul_add := sorry
-  add_smul := sorry
-  zero_smul := sorry
+  one_smul g := by ext; simp [smul_apply]
+  mul_smul r s g := by ext; simp [smul_apply, mul_smul]
+  smul_zero r := by ext; simp [smul_apply]
+  smul_add r f g := by ext; simp [smul_apply]
+  add_smul r s g := by ext; simp [smul_apply, add_smul]
+  zero_smul g := by ext; simp [smul_apply]
 
 
 end AutomorphicForm

blueprint/src/chapter/QuaternionAlgebraProject.tex

@@ -98,6 +98,7 @@ \section{Introduction and goal}
   \lean{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
   \label{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
   \uses{TotallyDefiniteQuaternionAlgebra.AutomorphicForm}
+  \leanok
   Pointwise addition $(f_1+f_2)(g):=f_1(g)+f_2(g)$ makes $S_{W,\chi}(U;R)$ into an additive
   abelian group.
 \end{definition}
@@ -107,6 +108,7 @@ \section{Introduction and goal}
   \label{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module}
   \uses{TotallyDefiniteQuaternionAlgebra.AutomorphicForm,
     TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
+  \leanok
   Pointwise scalar multiplication $(r\cdot f)(g):= r\cdot(f(g))$ makes
   $S_{W,\chi}(U;R)$ into an $R$-module.
 \end{definition}