aevalAeval — Mathlib

English

For x, y in A and a bivariate polynomial p ∈ R[X][Y], there is an R-algebra homomorphism sending p to p(x,y); this is the evaluation at the pair (x,y).

Русский

Для x, y ∈ A и двувариантного многочлена p ∈ R[X][Y] существует R-алгебра-хомоморфизм, отправляющий p в p(x,y); это вычисление в точке (x,y).

LaTeX

$$$\\text{aevalAeval}(x,y) : R[X][Y] \\to_{R} A \\,\\;\\text{ с }\\; p \\mapsto p(x,y)$$$

Lean4

/-- `aevalAeval x y` is the `R`-algebra evaluation morphism sending a two-variable polynomial
  `p : R[X][Y]` to `p(x,y)`. -/
abbrev aevalAeval (x y : A) : R[X][Y] →ₐ[R] A :=
  ((aeval x).restrictScalars R).comp
    (letI := Polynomial.algebra;
    (aeval (R := R[X]) (C y)).restrictScalars R)

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