Useful Notation

We define notation `R[X σ]` to be `MvPolynomial σ R`.

For a Finset `s` and a natural number `n`, we also define `s ^ᶠ n` to be
`Fintype.piFinset (fun (_ : Fin n) => s)`. This matches the intuition that `s ^ᶠ n`
is the set of all tuples of length `n` with elements in `s`.

def MvPolynomial.finOneEquiv (R : Type u_1) [CommSemiring R] : MvPolynomial (Fin 1) R ≃ₐ[R] Polynomial R

Equivalence between MvPolynomial (Fin 1) R and Polynomial R

def Polynomial.«term_⦃<_⦄[X]» : Lean.TrailingParserDescr

The R-submodule of R[X] consisting of polynomials of degree < n.

def Polynomial.«term_⦃≤_⦄[X]» : Lean.TrailingParserDescr

The R-submodule of R[X] consisting of polynomials of degree ≤ n.

def MvPolynomial.«term_[X_]» : Lean.TrailingParserDescr

Multivariate polynomial, where σ is the index set of the variables and R is the coefficient ring

def MvPolynomial.«term_⦃≤_⦄[X_]» : Lean.TrailingParserDescr

The submodule of polynomials such that the degree with respect to each individual variable is less than or equal to m.

def «term_^^_» : Lean.TrailingParserDescr

def «term_^ᶠ_» : Lean.TrailingParserDescr

def mvEval : Lean.TrailingParserDescr

Notation for multivariate polynomial evaluation. The expression p ⸨x_1, ..., x_n⸩ is expanded to the evaluation of p at the concatenated vectors x_1, ..., x_n, with the casting handled by omega. If omega fails, we can specify the proof manually using 'proof syntax.

For example, p ⸨x, y, z⸩ is expanded to MvPolynomial.eval (Fin.append (Fin.append x y) z ∘ Fin.cast (by omega)) p.

def mvEval' : Lean.TrailingParserDescr

Notation for multivariate polynomial evaluation. The expression p ⸨x_1, ..., x_n⸩ is expanded to the evaluation of p at the concatenated vectors x_1, ..., x_n, with the casting handled by omega. If omega fails, we can specify the proof manually using 'proof syntax.

For example, p ⸨x, y, z⸩ is expanded to MvPolynomial.eval (Fin.append (Fin.append x y) z ∘ Fin.cast (by omega)) p.

def mvEvalToPolynomial : Lean.TrailingParserDescr

Notation for evaluating a multivariate polynomial with one variable left intact. The expression p ⸨X ⦃i⦄, x_1, ..., x_n⸩ is expanded to the evaluation of p, viewed as a multivariate polynomial in all but the i-th variable, on the vector that is the concatenation of x_1, ..., x_n. Similar to mvEval syntax, casting between Fin types is handled by omega, or manually specified using 'proof syntax.

For example, p ⸨X ⦃i⦄, x, y⸩ is expanded to Polynomial.map (MvPolynomial.eval (Fin.append x y ∘ Fin.cast (by omega))) (MvPolynomial.finSuccEquivNth i p).

def mvEvalToPolynomial' : Lean.TrailingParserDescr

Notation for evaluating a multivariate polynomial with one variable left intact. The expression p ⸨X ⦃i⦄, x_1, ..., x_n⸩ is expanded to the evaluation of p, viewed as a multivariate polynomial in all but the i-th variable, on the vector that is the concatenation of x_1, ..., x_n. Similar to mvEval syntax, casting between Fin types is handled by omega, or manually specified using 'proof syntax.

For example, p ⸨X ⦃i⦄, x, y⸩ is expanded to Polynomial.map (MvPolynomial.eval (Fin.append x y ∘ Fin.cast (by omega))) (MvPolynomial.finSuccEquivNth i p).