mvPolynomial_aeval_coe — Mathlib

English

Let S be a subalgebra of A; for x: σ → S and p ∈ MvPolynomial σ R, the evaluation in A using x equals evaluation using x viewed as a map to A.

Русский

Пусть S — подалгебра A; для x: σ → S и p ∈ MvPolynomial σ R, вычисление в A по x эквивалентно вычислению по x, если x рассматривается как отображение в A.

LaTeX

$$$\operatorname{aeval} (\lambda i, (x_i : A)) p = \operatorname{aeval} x p$$$

Lean4

@[simp]
theorem mvPolynomial_aeval_coe (S : Subalgebra R A) (x : σ → S) (p : MvPolynomial σ R) :
    aeval (fun i => (x i : A)) p = aeval x p := by convert aeval_algebraMap_apply A x p

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