Setup for the polynomial tactic

This file initializes the environment extensions and simp sets used by the polynomial tactic.

These extensions let downstream users use their own polynomial-like types (such as PowerSeries) with the polynomial tactic suite.

opaque Mathlib.Tactic.Polynomial.polynomialPreExt : Lean.Meta.SimpExtension

polynomial_pre marks a theorem to be used by the polynomial tactic as a preprocessing lemma. These serve the purpose of removing any definitions specific to polynomials that algebra can't handle. e.g. Polynomial.C and Polynomial.map

opaque Mathlib.Tactic.Polynomial.polynomialPostExt : Lean.Meta.SimpExtension

polynomial_post marks a theorem to be used by the polynomial_nf tactic as a postprocessing lemma. Used only by polynomial_nf. These serve the purpose of rewriting expressions in algebra normal form into a more readable form. e.g. a • X -> algebraMap _ _ a * X -> C a * X.

def Mathlib.Tactic.Polynomial.PolyInferBaseAttr : Lean.ParserDescr

polynomial_infer_base marks a procedure used by the polynomial tactic to infer the base ring of polynomial-like types.

Equations

• Mathlib.Tactic.Polynomial.PolyInferBaseAttr = Lean.ParserDescr.node `Mathlib.Tactic.Polynomial.PolyInferBaseAttr 1024 (Lean.ParserDescr.nonReservedSymbol "polynomial_infer_base" false)

structure Mathlib.Tactic.Polynomial.PolynomialExt : Type

An extension for polynomial.

• infer : Lean.Expr → Lean.MetaM Lean.Expr

  Attempts to infer the base R of an Algebra R A based only on A. e.g. returns R given Polynomial R.

def Mathlib.Tactic.Polynomial.mkPolynomialExt (n : Lean.Name) : Lean.ImportM PolynomialExt

Read a polynomial extension from a declaration of the right type.

Equations

• One or more equations did not get rendered due to their size.

opaque Mathlib.Tactic.Polynomial.polynomialExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × PolynomialExt) (List Lean.Name × List (Lean.Name × PolynomialExt))

Environment extensions for polynomial declarations

def Mathlib.Tactic.Polynomial.inferBase (e : Lean.Expr) : Lean.MetaM Lean.Expr

Infer the base ring of Polynomial-like types that are registered using the polynomial environment extensions. Includes e.g. Polynomial and MvPolynomial.

Equations

• One or more equations did not get rendered due to their size.