def Lean.Meta.Grind.Arith.CommRing.mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr

def Lean.Grind.CommRing.Mon.findSimp? (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

Returns some c, where c is an equation from the basis whose leading monomial divides m. Remark: if the current ring does not satisfy the property

∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0

then the leading coefficient of the equation must also divide k

def Lean.Grind.CommRing.Mon.findSimp?.go (k : Int) (m : Mon) (checkCoeff noZeroDiv : Bool) : Mon → Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

def Lean.Grind.CommRing.Poly.findSimp? (p : Poly) : Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

Returns some c, where c is an equation from the basis whose leading monomial divides some monomial in p.

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyDerivation

Simplifies d.p using c, and returns an extended polynomial derivation.

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.simplify (d : PolyDerivation) : RingM PolyDerivation

Simplified d.p using the current basis, and returns the extended polynomial derivation.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyWithCore (c₁ c₂ : EqCnstr) : RingM (Option EqCnstr)

Simplifies c₁ using c₂.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyWith (c₁ c₂ : EqCnstr) : RingM EqCnstr

Simplifies c₁ using c₂.

partial def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyWithExhaustively (c₁ c₂ : EqCnstr) : RingM EqCnstr

Simplifies c₁ using c₂ exhaustively.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr

Simplify the given equation constraint using the current basis.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.checkConstant (c : EqCnstr) : RingM Bool

Returns true if c.p is the constant polynomial.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyAndCheck (c : EqCnstr) : RingM (Option EqCnstr)

Simplifies and checks whether the resulting constraint is trivial (i.e., 0 = 0), or inconsistent (i.e., k = 0 where k % c != 0 for a comm-ring with characteristic c), and returns none. Otherwise, returns the simplified constraint.

def Lean.Meta.Grind.Arith.CommRing.addToBasisCore (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToQueue (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.superposeWith (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.superposeWith.go (c : EqCnstr) : Mon → RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toMonic (c : EqCnstr) : RingM EqCnstr

Tries to convert the leading monomial into a monic one.

It exploits the fact that given a polynomial with leading coefficient k, if the ring has a nonzero characteristic p and gcd k p = 1, then k has an inverse.

It also handles the easy case where k is -1.

Remark: if the ring implements the class NoNatZeroDivisors, then the coefficients are divided by the gcd of all coefficients.

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyBasis.go (c : EqCnstr) (m m' : Mon) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyBasis.goVar (c : EqCnstr) (m : Mon) (x : Var) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToBasis (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.addNewEq (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.checkConstant (c : DiseqCnstr) : RingM Bool

Returns true if c.d.p is the constant polynomial.

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.simplify (c : DiseqCnstr) : RingM DiseqCnstr

def Lean.Meta.Grind.Arith.CommRing.saveDiseq (c : DiseqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.addNewDiseq (c : DiseqCnstr) : RingM Unit

@[export lean_process_ring_eq]

def Lean.Meta.Grind.Arith.CommRing.processNewEqImpl (a b : Expr) : GoalM Unit

@[export lean_process_ring_diseq]

def Lean.Meta.Grind.Arith.CommRing.processNewDiseqImpl (a b : Expr) : GoalM Unit

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.PropagateEqMap : Type

def Lean.Meta.Grind.Arith.CommRing.checkRing : RingM Bool

def Lean.Meta.Grind.Arith.CommRing.check : GoalM Bool