aeval_algebraMap_apply_eq_algebraMap_eval

English

For any x ∈ R, aeval(algebraMap_R_A x) p = algebraMap_R_A (p.eval x).

Русский

Для любых x ∈ R выполняется aeval(algebraMap_R_A x) p = algebraMap_R_A (p.eval x).

LaTeX

$$$\forall x\in R:\; \operatorname{aeval}(\operatorname{algebraMap} R A x) p = \operatorname{algebraMap} R A (p.eval x).$$$

Lean4

theorem aeval_algebraMap_apply_eq_algebraMap_eval (x : R) (p : R[X]) :
    aeval (algebraMap R A x) p = algebraMap R A (p.eval x) :=
  aeval_algHom_apply (Algebra.ofId R A) x p

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