aeval_algebraMap_apply — Mathlib

English

For any i, the evaluation of p under the composition algebraMap A B ∘ x equals applying algebraMap A B to the evaluation of p under x.

Русский

Для любого i, вычисление p под композицией algebraMap A B ∘ x эквивалентно применению algebraMap A B к вычислению p по x.

LaTeX

$$$\operatorname{aeval} (\operatorname{algebraMap} A B \circ x) p = \operatorname{algebraMap} A B \big( \operatorname{aeval} x p \big)$$$

Lean4

theorem aeval_algebraMap_apply (x : σ → A) (p : MvPolynomial σ R) :
    aeval (algebraMap A B ∘ x) p = algebraMap A B (MvPolynomial.aeval x p) := by
  rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ← IsScalarTower.algebraMap_eq,
    Function.comp_def]

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