Documentation

Mathlib.Tactic.Ring.NamePolyVars

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.
    Instances For