def Lean.Meta.Grind.Arith.CommRing.get' : GoalM State

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modify' (f : State → State) : GoalM Unit

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

def Lean.Meta.Grind.Arith.CommRing.incSteps : 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.

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

• getRing : m Ring

@[always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetRing m] : MonadGetRing n

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

def Lean.Meta.Grind.Arith.CommRing.RingM.getRing : RingM Ring

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM : MonadGetRing RingM

@[inline]

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

@[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.setTermRingId (e : Expr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.nonzeroChar? {m : Type → Type} [Monad m] [MonadGetRing 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] [MonadGetRing 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.Grind.CommRing.Expr.toPolyM (e : Meta.Grind.Arith.CommRing.RingExpr) : Meta.Grind.Arith.CommRing.RingM Poly

Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization.

def Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : Meta.Grind.Arith.CommRing.RingM Poly

def Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM Poly

def Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

def Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

def Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM SPolResult

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

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