Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.Poly

@[irreducible]

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

Equations
@[irreducible]

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

Equations

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

Equations

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
@[irreducible]

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

Equations

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.mulMon' (p : Poly) (k : Int) (m : Mon) (char? : Option Nat := none) :
Equations
def Lean.Grind.CommRing.Poly.combine' (p₁ p₂ : Poly) (char? : Option Nat := none) :
Equations

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? = { }

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

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
def Lean.Grind.CommRing.Poly.simp?.go? (char? : Option Nat := none) (k₂' : Int) (m₂ : Mon) (p₂ p₁ : Poly) :
Equations

Returns true if the leading monomial of p divides m.

Equations

Returns the leading coefficient of the given polynomial

Equations

Returns the leading monomial of the given polynomial.

Equations