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

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

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