Documentation
Toric
.
Mathlib
.
Algebra
.
Polynomial
.
Bivariate
Search
return to top
source
Imports
Init
Mathlib.Algebra.Polynomial.Bivariate
Imported by
Polynomial
.
aevalAEval
Polynomial
.
aevalAEval_X
Polynomial
.
aevalAEval_Y
source
noncomputable def
Polynomial
.
aevalAEval
{
R
:
Type
u_1}
{
A
:
Type
u_2}
[
CommRing
R
]
[
CommRing
A
]
[
Algebra
R
A
]
(
x
y
:
A
)
:
Polynomial
(
Polynomial
R
)
→ₐ[
R
]
A
Equations
One or more equations did not get rendered due to their size.
Instances For
source
@[simp]
theorem
Polynomial
.
aevalAEval_X
{
R
:
Type
u_1}
{
A
:
Type
u_2}
[
CommRing
R
]
[
CommRing
A
]
[
Algebra
R
A
]
(
x
y
:
A
)
:
(
aevalAEval
x
y
)
X
=
x
source
@[simp]
theorem
Polynomial
.
aevalAEval_Y
{
R
:
Type
u_1}
{
A
:
Type
u_2}
[
CommRing
R
]
[
CommRing
A
]
[
Algebra
R
A
]
(
x
y
:
A
)
:
(
aevalAEval
x
y
)
(
C
X
)
=
y