smul_eval_smul — Mathlib

English

The polynomial defined as the product of distinct linear factors (X − g • x) over the quotient by the stabilizer is monic.

Русский

Полином, получающийся как произведение различных линейных множителей (X − g • x) по фактору по стабилизатору, моничен.

LaTeX

$$$\bigl(prodXSubSMul G R x\bigr).Monic$.$$

Lean4

theorem smul_eval_smul (m : M) (f : S[X]) (x : S) : (m • f).eval (m • x) = m • f.eval x :=
  Polynomial.induction_on f (fun r ↦ by rw [smul_C, eval_C, eval_C])
    (fun f g ihf ihg ↦ by rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]) fun n r _ ↦ by
    rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C, eval_X_pow, smul_mul',
      smul_pow']

Похожие утверждения