The command name_power_vars names variables in MvPowerSeries (Fin n) R for the appropriate value of n. The notation introduced by this command is local.

Usage:

variable (R : Type) [CommRing R]

name_power_vars X, Y, Z over R

#check Y -- Y : MvPowerSeries (Fin 3) R

def Mathlib.Tactic.namePowerVarsOver : Lean.ParserDescr

The command name_power_vars names variables in MvPowerSeries (Fin n) R for the appropriate value of n. The notation introduced by this command is local.

Usage:

variable (R : Type) [CommRing R]

name_power_vars X, Y, Z over R

#check Y -- Y : MvPowerSeries (Fin 3) R

def Mathlib.Tactic.elabNamePowerSeriesVariablesOver : Lean.Elab.Command.CommandElab

The command name_power_vars names variables in MvPowerSeries (Fin n) R for the appropriate value of n. The notation introduced by this command is local.

Usage:

variable (R : Type) [CommRing R]

name_power_vars X, Y, Z over R

#check Y -- Y : MvPowerSeries (Fin 3) R