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

Instances For

source
@[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✝

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

- pw.toExpr = if (pw.k == 1) = true then Lean.Grind.CommRing.Expr.var pw.x else (Lean.Grind.CommRing.Expr.var pw.x).pow pw.k

Instances For

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

- Lean.Grind.CommRing.Mon.unit.toExpr = Lean.Grind.CommRing.Expr.num 1
- (Lean.Grind.CommRing.Mon.mult p m_1).toExpr = Lean.Grind.CommRing.Mon.toExpr.go✝ m_1 p.toExpr

Instances For

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

- (Lean.Grind.CommRing.Poly.num k).toExpr = Lean.Grind.CommRing.Expr.num k
- (Lean.Grind.CommRing.Poly.add k m p_1).toExpr = Lean.Grind.CommRing.Poly.toExpr.go✝ p_1 (Lean.Grind.CommRing.Poly.toExpr.goTerm✝ k m)

Instances For