fix blueprint

Author: kbuzzard

blueprint/lean_decls

@@ -59,11 +59,17 @@ AutomorphicForm.GLn.IsSmooth
 AutomorphicForm.GLn.IsSlowlyIncreasing
 AutomorphicForm.GLn.Weight
 AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
-Pointwise.stabilizer.toGaloisGroup
-MulAction.stabilizer_surjective_of_action
+Bourbaki52222.stabilizer.toGaloisGroup
+Bourbaki52222.MulAction.stabilizer_surjective_of_action
 MulSemiringAction.CharacteristicPolynomial.F
 MulSemiringAction.CharacteristicPolynomial.M
 MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero
 MulSemiringAction.CharacteristicPolynomial.M_deg
 MulSemiringAction.CharacteristicPolynomial.M_monic
-MulSemiringAction.CharacteristicPolynomial.isIntegral
+MulSemiringAction.CharacteristicPolynomial.isIntegral
+MulSemiringAction.CharacteristicPolynomial.Mbar
+MulSemiringAction.CharacteristicPolynomial.Mbar_deg
+MulSemiringAction.CharacteristicPolynomial.Mbar_monic
+MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero
+MulSemiringAction.reduction_isIntegral
+Algebra.exists_dvd_nonzero_if_isIntegral

blueprint/src/chapter/FrobeniusProject.tex

@@ -29,8 +29,8 @@ \section{Statement of the theorem}
 In the next definition we write down a group homomorphism $\phi$ from $D_Q$ to $\Aut_K(L)$.
 
 \begin{definition}
-  \label{Pointwise.stabilizer.toGaloisGroup}
-  \lean{Pointwise.stabilizer.toGaloisGroup}
+  \label{Bourbaki52222.stabilizer.toGaloisGroup}
+  \lean{Bourbaki52222.stabilizer.toGaloisGroup}
   Choose $g\in D_Q$. Then the action of $g$ on $B$ gives us an induced
   $A/P$-algebra automorphism of $B/Q$ which extends to a $K$-algebra automorphism $\phi(g)$ of $L$.
   This construction $g\mapsto \phi(g)$ defines a group homomorphism from $D_Q$
@@ -40,9 +40,9 @@ \section{Statement of the theorem}
 
 The theorem we want in this project is
 \begin{theorem}
-  \label{MulAction.stabilizer_surjective_of_action}
-  \lean{MulAction.stabilizer_surjective_of_action}
-  \uses{Pointwise.stabilizer.toGaloisGroup}
+  \label{Bourbaki52222.MulAction.stabilizer_surjective_of_action}
+  \lean{Bourbaki52222.MulAction.stabilizer_surjective_of_action}
+  \uses{Bourbaki52222.stabilizer.toGaloisGroup}
   The map $g\mapsto \phi_g$ from $D_Q$ to $\Aut_K(L)$ defined above is surjective.
 \end{theorem}