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

source
def Mathlib.Tactic.namePolyVarsOver :
Lean.ParserDescr

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

source
def Mathlib.Tactic.elabNameVariablesOver :
Lean.Elab.Command.CommandElab

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