aeval_sumIDeriv_eq_eval — Mathlib

English

For p ∈ R[X], r ∈ A, we have aeval r (sumIDeriv p) = eval r (sumIDeriv (map(algebraMap R A) p)).

Русский

Для p ∈ R[X] и r ∈ A имеет место aeval_r(sumIDeriv p) = eval_r(sumIDeriv(map(algebraMap R A) p)).

LaTeX

$$$$ \mathrm{aeval}_r(\sumIDeriv p) = \mathrm{eval}_r(\sumIDeriv(p.map(\mathrm{algebraMap}\ R\ A))). $$$$

Lean4

theorem aeval_sumIDeriv_eq_eval (p : R[X]) (r : A) :
    aeval r (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p)) := by
  rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]

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