English
Polynomials over FixedPoints.subfield are fixed under the monoid action; smul distributes through polynomial operations.
Русский
Полиномы над FixedPoints.subfield фиксированы относительно действия моноида; умножение на элемент моноида распространяется на полиномы.
LaTeX
$$$ (m:\\mathrm{M}) \\cdot p = p \\text{ for all } p \\in \\mathrm{Polynomial}(\\mathrm{FixedPoints.subfield} M F) $$$
Lean4
@[simp]
theorem smul_polynomial (m : M) (p : Polynomial (FixedPoints.subfield M F)) : m • p = p :=
Polynomial.induction_on p (fun x => by rw [Polynomial.smul_C, smul]) (fun p q ihp ihq => by rw [smul_add, ihp, ihq])
fun n x _ => by rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
