scaleRoots_aeval_eq_zero — Mathlib

English

For a ring hom f, r ∈ R, s ∈ S, the evaluation of scaleRoots satisfies eval₂ f (f s · r) (scaleRoots p s) = f s^{natDegree(p)} · eval₂ f r p.

Русский

Для кольцевого отображения f; r, s; eval₂ f (f s · r) (scaleRoots p s) = f s^{natDegree(p)} · eval₂ f r p.

LaTeX

$$$\operatorname{eval}_2 f (f s \cdot r) (\operatorname{scaleRoots}(p, s)) = (f s)^{p.\operatorname{natDegree}} \cdot \operatorname{eval}_2 f r p$$$

Lean4

theorem scaleRoots_aeval_eq_zero [Algebra R A] {p : R[X]} {a : A} {r : R} (ha : aeval a p = 0) :
    aeval (algebraMap R A r * a) (scaleRoots p r) = 0 :=
  by
  rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]
  · apply Algebra.commutes
  · intros; rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]

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