aeval_coe — Mathlib

English

Compatibility of polynomial evaluation with scalar restriction: evaluating a polynomial P at x ∈ S, considered inside L, yields the same result as evaluating P at x with the restricted scalars.

Русский

Совместимость вычисления многочлена: вычисление P при x ∈ S в L равно вычислению P при x с ограниченными скалярами.

LaTeX

$$$ aeval_L(x) P = aeval_S(x) P $$$

Lean4

theorem aeval_coe {R : Type*} [CommSemiring R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] (x : S) (P : R[X]) :
    aeval (x : L) P = aeval x P :=
  aeval_algHom_apply (S.val.restrictScalars R) x P

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