The command name_poly_vars
names variables in
MvPolynomial (Fin n) R
for the appropriate value of n
.
The notation introduced by this command is local.
Usage:
variable (R : Type) [CommRing R]
name_poly_vars X, Y, Z over R
#check Y -- Y : MvPolynomial (Fin 3) R
The command name_poly_vars
names variables in
MvPolynomial (Fin n) R
for the appropriate value of n
.
The notation introduced by this command is local.
Usage:
variable (R : Type) [CommRing R]
name_poly_vars X, Y, Z over R
#check Y -- Y : MvPolynomial (Fin 3) R
Equations
- One or more equations did not get rendered due to their size.
Instances For
The command name_poly_vars
names variables in
MvPolynomial (Fin n) R
for the appropriate value of n
.
The notation introduced by this command is local.
Usage:
variable (R : Type) [CommRing R]
name_poly_vars X, Y, Z over R
#check Y -- Y : MvPolynomial (Fin 3) R
Equations
- One or more equations did not get rendered due to their size.