The polynomial functions at Poly.lean are used for constructing proofs-by-reflection, but they do not provide mechanisms for aborting expensive computations.

@[reducible, inline]

abbrev Lean.Grind.CommRing.Expr.toPolyM (e : Meta.Grind.Arith.CommRing.RingExpr) : Meta.Grind.Arith.CommRing.RingM Poly

Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization.

Equations

• Lean.Grind.CommRing.Expr.toPolyM e = Lean.Meta.Grind.Arith.CommRing.toPoly✝ e

@[reducible, inline]

abbrev Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p.mulConstM k = Lean.Meta.Grind.Arith.CommRing.mulConst✝ k p

@[reducible, inline]

abbrev Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p.mulMonM k m = Lean.Meta.Grind.Arith.CommRing.mulMon✝ k m p

@[reducible, inline]

abbrev Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p₁.mulM p₂ = Lean.Meta.Grind.Arith.CommRing.mul✝ p₁ p₂

@[reducible, inline]

abbrev Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p₁.combineM p₂ = Lean.Meta.Grind.Arith.CommRing.combine✝ p₁ p₂

def Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM SPolResult

Equations

• One or more equations did not get rendered due to their size.
• p₁.spolM p₂ = pure { }