FROBENIUS: reduction of char poly from B to B/Q

[kbuzzard]

The issue: fill in the following sorries: Mbar_deg, Mbar_monic, Mbar_eval_eq_zero , reduction_isIntegral in the MulSemiringAction.CharacteristicPolynomial namespace (probably they should be in this Bourbaki52222 namespace).

The three sorries Mbar_deg, Mbar_monic, Mbar_eval_eq_zero are all mathematically simple deductions from the fact that we have a polynomial $M_b$ in A[X] which is monic of degree |G| and satisfies $M_b(b)=0$. We reduce $M_b$ mod $P$ to get $\overline{M}_b\in (A/P)[X]$, and we need to prove that this polynomial is also monic of degree $|G|$ and has $b$ as a root.

reduction_isIntegral follows easily from this.

[AlexBrodbelt]

can I claim the remainder of sorries?

[Ruben-VandeVelde]

@AlexBrodbelt I apologise - I only saw your comment after finishing the proof of Mbar_eval_eq_zero, which I'll push in a bit.

[AlexBrodbelt]

No worries :), I was going to be slow anyway.