@[irreducible]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.sharesVar x✝ = false
• x✝.sharesVar Lean.Grind.CommRing.Mon.unit = false

@[irreducible]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.lcm x✝ = x✝
• x✝.lcm Lean.Grind.CommRing.Mon.unit = x✝

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.divides x✝ = true
• x✝.divides Lean.Grind.CommRing.Mon.unit = false

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

Equations

• One or more equations did not get rendered due to their size.
• x✝.div Lean.Grind.CommRing.Mon.unit = x✝
• Lean.Grind.CommRing.Mon.unit.div x✝ = Lean.Grind.CommRing.Mon.unit

@[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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.coprime x✝ = true
• x✝.coprime Lean.Grind.CommRing.Mon.unit = true

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

Equations

• p.mulConst' k (some char) = Lean.Grind.CommRing.Poly.mulConstC k p char
• p.mulConst' k char? = Lean.Grind.CommRing.Poly.mulConst k p

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

Equations

• p.mulMon' k m (some char) = Lean.Grind.CommRing.Poly.mulMonC k m p char
• p.mulMon' k m char? = Lean.Grind.CommRing.Poly.mulMon k m p

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

Equations

• p₁.combine' p₂ (some char) = p₁.combineC p₂ char
• p₁.combine' p₂ char? = p₁.combine p₂

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.

Equations

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

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.

Equations

• p₁.simp? (Lean.Grind.CommRing.Poly.add k₂' m₂ p₂_2) char? = Lean.Grind.CommRing.Poly.simp?.go? char? k₂' m₂ p₂_2 p₁
• p₁.simp? p₂ char? = none

def Lean.Grind.CommRing.Poly.simp?.go? (char? : Option Nat := none) (k₂' : Int) (m₂ : Mon) (p₂ p₁ : Poly) : Option SimpResult

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.simp?.go? char? k₂' m₂ p₂ (Lean.Grind.CommRing.Poly.num k) = none

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

Equations

• (Lean.Grind.CommRing.Poly.num k).degree = 0
• (Lean.Grind.CommRing.Poly.add k m p).degree = m.degree

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

Returns true if the leading monomial of p divides m.

Equations

• (Lean.Grind.CommRing.Poly.num k).divides m = true
• (Lean.Grind.CommRing.Poly.add k m_1 p_1).divides m = m_1.divides m

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

Returns the leading coefficient of the given polynomial

Equations

• (Lean.Grind.CommRing.Poly.num k).lc = k
• (Lean.Grind.CommRing.Poly.add k m p).lc = k

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

Returns the leading monomial of the given polynomial.

Equations

• (Lean.Grind.CommRing.Poly.num k).lm = Lean.Grind.CommRing.Mon.unit
• (Lean.Grind.CommRing.Poly.add k m p).lm = m

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

Equations

• (Lean.Grind.CommRing.Poly.num 0).isZero = true
• x✝.isZero = false

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

Equations

• (Lean.Grind.CommRing.Poly.num k).checkCoeffs = true
• (Lean.Grind.CommRing.Poly.add k m p).checkCoeffs = (k != 0 && p.checkCoeffs)

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

Equations

• (Lean.Grind.CommRing.Poly.num k).checkNoUnitMon = true
• (Lean.Grind.CommRing.Poly.add k Lean.Grind.CommRing.Mon.unit p).checkNoUnitMon = false
• (Lean.Grind.CommRing.Poly.add k v p).checkNoUnitMon = p.checkNoUnitMon

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

Equations

• (Lean.Grind.CommRing.Poly.num k).gcdCoeffs = k.natAbs
• (Lean.Grind.CommRing.Poly.add k m p).gcdCoeffs = Lean.Grind.CommRing.Poly.gcdCoeffs.go p k.natAbs

def Lean.Grind.CommRing.Poly.gcdCoeffs.go (p : Poly) (acc : Nat) : Nat

Equations

• Lean.Grind.CommRing.Poly.gcdCoeffs.go (Lean.Grind.CommRing.Poly.num k) acc = if (acc == 1) = true then acc else acc.gcd k.natAbs
• Lean.Grind.CommRing.Poly.gcdCoeffs.go (Lean.Grind.CommRing.Poly.add k m p_1) acc = if (acc == 1) = true then acc else Lean.Grind.CommRing.Poly.gcdCoeffs.go p_1 (acc.gcd k.natAbs)

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

Equations

• (Lean.Grind.CommRing.Poly.num k).divConst a = Lean.Grind.CommRing.Poly.num (k / a)
• (Lean.Grind.CommRing.Poly.add k m p_1).divConst a = Lean.Grind.CommRing.Poly.add (k / a) m (p_1.divConst a)

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

Equations

• Lean.Grind.CommRing.Mon.unit.size = 0
• (Lean.Grind.CommRing.Mon.mult p m).size = m.size + 1

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

Equations

• (Lean.Grind.CommRing.Poly.num k).size = 1
• (Lean.Grind.CommRing.Poly.add k m p).size = m.size + 1 + p.size

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

Equations

• (Lean.Grind.CommRing.Poly.num k).length = 0
• (Lean.Grind.CommRing.Poly.add k m p).length = 1 + p.length