@[irreducible]

def Lean.Grind.CommRing.Mon.sharesVar : Mon → Mon → Bool

sharesVar m₁ m₂ returns true if m₁ and m₂ shares at least one variable.

@[irreducible]

def Lean.Grind.CommRing.Mon.lcm : Mon → Mon → Mon

lcm m₁ m₂ returns the least common multiple of the given monomials.

def Lean.Grind.CommRing.Mon.divides : Mon → Mon → Bool

divides m₁ m₂ returns true if monomial m₁ divides m₂ Example: x^2.z divides w.x^3.y^2.z

def Lean.Grind.CommRing.Mon.div : Mon → Mon → Mon

Given m₁ and m₂ such that m₂.divides m₁, then m₁.div m₂ returns the result. Example w.x^3.y^2.z div x^2.z returns w.x.y^2

@[irreducible]

def Lean.Grind.CommRing.Mon.coprime : Mon → Mon → Bool

coprime m₁ m₂ returns true if the given monomials do not have any variable in common.

structure Lean.Grind.CommRing.SPolResult : Type

Contains the S-polynomial resulting from superposing two polynomials p₁ and p₂, along with coefficients and monomials used in their construction.

• spol : Poly

  The computed S-polynomial.

• k₁ : Int

  Coefficient applied to polynomial p₁.

• m₁ : Mon

  Monomial factor applied to polynomial p₁.

• k₂ : Int

  Coefficient applied to polynomial p₂.

• m₂ : Mon

  Monomial factor applied to polynomial p₂.

def Lean.Grind.CommRing.Poly.mulConst' (p : Poly) (k : Int) (char? : Option Nat := none) : Poly

def Lean.Grind.CommRing.Poly.mulMon' (p : Poly) (k : Int) (m : Mon) (char? : Option Nat := none) : Poly

def Lean.Grind.CommRing.Poly.combine' (p₁ p₂ : Poly) (char? : Option Nat := none) : Poly

def Lean.Grind.CommRing.Poly.spol (p₁ p₂ : Poly) (char? : Option Nat := none) : SPolResult

Returns the S-polynomial of polynomials p₁ and p₂, and coefficients&terms used to construct it. Given polynomials with leading terms k₁*m₁ and k₂*m₂, the S-polynomial is defined as:

S(p₁, p₂) = (k₂/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₁) * p₁ - (k₁/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₂) * p₂

Remark: if char? = some c, then c is the characteristic of the ring.

structure Lean.Grind.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.simp? (p₁ p₂ : Poly) (char? : Option Nat := none) : Option 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₂.

Remark: if char? = some c, then c is the characteristic of the ring.

def Lean.Grind.CommRing.Poly.degree : Poly → Nat

def Lean.Grind.CommRing.Poly.divides (p : Poly) (m : Mon) : Bool

Returns true if the leading monomial of p divides m.

def Lean.Grind.CommRing.Poly.lc : Poly → Int

Returns the leading coefficient of the given polynomial

def Lean.Grind.CommRing.Poly.lm : Poly → Mon

Returns the leading monomial of the given polynomial.

def Lean.Grind.CommRing.Poly.isZero : Poly → Bool

def Lean.Grind.CommRing.Poly.getConst : Poly → Int

def Lean.Grind.CommRing.Poly.checkCoeffs : Poly → Bool

def Lean.Grind.CommRing.Poly.checkNoUnitMon : Poly → Bool

def Lean.Grind.CommRing.Poly.gcdCoeffs : Poly → Nat

def Lean.Grind.CommRing.Poly.divConst (p : Poly) (a : Int) : Poly

def Lean.Grind.CommRing.Mon.size : Mon → Nat

def Lean.Grind.CommRing.Poly.size : Poly → Nat

def Lean.Grind.CommRing.Poly.length : Poly → Nat

def Lean.Grind.CommRing.Power.toExpr (pw : Power) : Expr

def Lean.Grind.CommRing.Mon.toExpr (m : Mon) : Expr

def Lean.Grind.CommRing.Poly.toExpr (p : Poly) : Expr

def Lean.Grind.CommRing.Poly.maxDegreeOf (p : Poly) (x : Var) : Nat