Bivariate polynomials #
This file introduces the notation R[X][Y]
for the polynomial ring R[X][X]
in two variables,
and the notation Y
for the second variable, in the Polynomial
scope.
It also defines Polynomial.evalEval
for the evaluation of a bivariate polynomial at a point
on the affine plane, which is a ring homomorphism (Polynomial.evalEvalRingHom
), as well as
the abbreviation CC
to view a constant in the base ring R
as a bivariate polynomial.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The notation Y
for X
in the Polynomial
scope.
Equations
- Polynomial.termY = Lean.ParserDescr.node `Polynomial.termY 1024 (Lean.ParserDescr.symbol "Y")
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The notation R[X][Y]
for R[X][X]
in the Polynomial
scope.
Equations
- Polynomial.«term_[X][Y]» = Lean.ParserDescr.trailingNode `Polynomial.term_[X][Y] 1024 0 (Lean.ParserDescr.symbol "[X][Y]")
Instances For
evalEval x y p
is the evaluation p(x,y)
of a two-variable polynomial p : R[X][Y]
.
Equations
- Polynomial.evalEval x y p = Polynomial.eval x (Polynomial.eval (Polynomial.C y) p)
Instances For
A constant viewed as a polynomial in two variables.
Equations
- Polynomial.CC r = Polynomial.C (Polynomial.C r)
Instances For
evalEval x y
as a ring homomorphism.
Equations
- Polynomial.evalEvalRingHom x y = (Polynomial.evalRingHom x).comp (Polynomial.evalRingHom (Polynomial.C y))
Instances For
Two equivalent ways to express the evaluation of a bivariate polynomial over R
at a point in the affine plane over an R
-algebra S
.
Viewing R[X,Y,X']
as an R[X']
-algebra, a polynomial p : R[X',Y']
can be evaluated at
Y : R[X,Y,X']
(substitution of Y'
by Y
), obtaining another polynomial in R[X,Y,X']
.
When this polynomial is then evaluated at X' = X
, the original polynomial p
is recovered.
If the evaluation (evalEval
) of a bivariate polynomial p : R[X][Y]
at a point (x,y)
is zero, then Polynomial.evalEval x y
factors through AdjoinRoot.evalEval
, a ring homomorphism
from AdjoinRoot p
to R
.