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

@[inline]

def Lean.Grind.CommRing.Expr.toPolyM? (e : Meta.Grind.Arith.CommRing.RingExpr) : Meta.Grind.Arith.CommRing.RingM (Option 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

@[inline]

def 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

@[inline]

def 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

@[inline]

def 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₂

@[inline]

def 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 { }

def Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) : Meta.Grind.Arith.CommRing.RingM (Option (Nat × Var))

Returns some (val, x) if m contains a variable x whose the denotation is val⁻¹.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.findInvNumeralVar? = pure none

def Lean.Grind.CommRing.Poly.findInvNumeralVar? (p : Poly) : Meta.Grind.Arith.CommRing.RingM (Option (Nat × Var))

Returns some (val, x) if p contains a variable x whose the denotation is val⁻¹.

Equations

• (Lean.Grind.CommRing.Poly.num k).findInvNumeralVar? = pure none
• (Lean.Grind.CommRing.Poly.add k m p₁_1).findInvNumeralVar? = do let __x ← m.findInvNumeralVar? match __x with | some r => pure (some r) | x => p₁_1.findInvNumeralVar?

structure Lean.Meta.Grind.Arith.CommRing.SimpResult : Type

Result of simplifying a polynomial p₁ using a polynomial p₂.

The simplification rewrites the first monomial of p₁ that can be divided by the leading monomial of p₂.

• p : Poly

  The resulting simplified polynomial after rewriting.

• k₁ : Int

  The integer coefficient multiplied with polynomial p₁ in the rewriting step.

• k₂ : Int

  The integer coefficient multiplied with polynomial p₂ during rewriting.

• m₂ : Mon

  The monomial factor applied to polynomial p₂.

def Lean.Grind.CommRing.Poly.simpM? (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.SimpResult)

Simplifies polynomial p₁ using polynomial p₂ by rewriting.

This function attempts to rewrite p₁ by eliminating the first occurrence of the leading monomial of p₂.

If checkCoeffDvd is true (and the ring does not implement NoNatZeroDivisors), a monomial is rewritten only if its coefficient is divisible by the leading coefficient of p₂, i.e., only if the rewrite does not multiply p₁ by a constant k₁ ≠ ±1. See RingM.Context.checkCoeffDvd.

Equations

• One or more equations did not get rendered due to their size.
• p₁.simpM? p₂ = pure none