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

def Lean.Meta.Grind.Arith.CommRing.checkMaxDegree (p : Poly) : GoalM Bool

def Lean.Meta.Grind.Arith.CommRing.incSteps (n : Nat := 1) : GoalM Unit

structure Lean.Meta.Grind.Arith.CommRing.RingM.Context : Type

• ringId : Nat
• checkCoeffDvd : Bool

  If checkCoeffDvd is true, then when using a polynomial k*m - p to simplify .. + k'*m*m_2 + ..., the substitution is performed IF

  • k divides k', OR
  • Ring implements NoNatZeroDivisors.

  We need this check when simplifying disequalities. In this case, if we perform the simplification anyway, we may end up with a proof that k * q = 0, but we cannot deduce q = 0 since the ring does not implement NoNatZeroDivisors See comment at PolyDerivation.

  We also need it when destructively simplifying equations, i.e., when replacing an equation with its simplified form (EqCnstr.simplify and EqCnstr.simplifyBasis): the rewrite multiplies the equation by k₁ = k/gcd k k', and the result is weaker than the original equation when k₁ ≠ ±1. See Note at EqCnstr.simplify.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.RingM (α : Type) : Type

We don't want to keep carrying the RingId around.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.RingM.run {α : Type} (ringId : Nat) (x : RingM α) : GoalM α

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getRingId : RingM Nat

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonRingM : Sym.Arith.MonadCanon RingM

def Lean.Meta.Grind.Arith.CommRing.RingM.getCommRing : RingM CommRing

def Lean.Meta.Grind.Arith.CommRing.RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingRingM : MonadCommRing RingM

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd {α : Type} (x : RingM α) : RingM α

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

def Lean.Meta.Grind.Arith.CommRing.getTermRingId? (e : Expr) : GoalM (Option Nat)

def Lean.Meta.Grind.Arith.CommRing.nonzeroChar? {m : Type → Type} [Monad m] [MonadRing m] : m (Option Nat)

Returns some c if the current ring has a nonzero characteristic c.

def Lean.Meta.Grind.Arith.CommRing.nonzeroCharInst? {m : Type → Type} [Monad m] [MonadRing m] : m (Option (Expr × Nat))

Returns some (charInst, c) if the current ring has a nonzero characteristic c.

def Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? : RingM (Option Expr)

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

Returns true if the current ring satisfies the property

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

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

Returns true if the current ring has a IsCharP instance.

def Lean.Meta.Grind.Arith.CommRing.getCharInst : RingM (Expr × Nat)

Returns the pair (charInst, c). If the ring does not have a IsCharP instance, then throws internal error.

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

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

def Lean.Meta.Grind.Arith.CommRing.getNext? : RingM (Option EqCnstr)

class Lean.Meta.Grind.Arith.CommRing.MonadSetTermId (m : Type → Type) : Type

• setTermId : Expr → m Unit

def Lean.Meta.Grind.Arith.CommRing.setTermRingId (e : Expr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.mkVarCore {m : Type → Type} [MonadLiftT GoalM m] [Monad m] [MonadRing m] [MonadSetTermId m] (e : Expr) : m Var

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdRingM : MonadSetTermId RingM

def Lean.Meta.Grind.Arith.CommRing.mkVar (e : Expr) : RingM Var