def Lean.Meta.Grind.Arith.CommRing.mkUnaryFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.mkBinHomoFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.mkPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.mkNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getAddFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getSubFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getMulFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getNegFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getOne {m : Type → Type} [Monad m] [MonadCanon m] [MonadRing m] [MonadLiftT GoalM m] : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CommRing.getInvFn {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] : m Expr

Equations

• One or more equations did not get rendered due to their size.