aeval_eq_of_algebra — Mathlib

English

For a polynomial p over R[X] and root α in AdjoinRoot root f, evaluating p at α coincides with mk f applied to map(algebraMap) p.

Русский

Пришел полином p над R[X] и корень α в AdjoinRoot, вычисление p(α) совпадает с mk f (map(algebraMap p)).

LaTeX

$$aeval(root f) p = mk f (map (algebraMap R S) p)$$

Lean4

theorem aeval_eq_of_algebra [CommRing S] [Algebra R S] (f : S[X]) (p : R[X]) :
    aeval (root f) p = mk f (map (algebraMap R S) p) := by
  induction p using Polynomial.induction_on with
  | C a =>
    simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp
  | add p q _ _ => simp_all
  | monomial n a _ => simp_all [pow_add, ← mul_assoc]

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