# Instances for `grind`. #

source
@[instance 100]
instance Semiring.toGrindSemiring (α : Type u_1) [s : Semiring α] :
Lean.Grind.Semiring α
Equations

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

source
@[instance 100]
instance CommSemiring.toGrindCommSemiring (α : Type u_1) [s : CommSemiring α] :
Lean.Grind.CommSemiring α
Equations

- CommSemiring.toGrindCommSemiring α = { toSemiring := Semiring.toGrindSemiring α, mul_comm := ⋯ }

source
@[instance 100]
instance Ring.toGrindRing (α : Type u_1) [s : Ring α] :
Lean.Grind.Ring α
Equations

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

source
@[instance 100]
instance CommRing.toGrindCommRing (α : Type u_1) [s : CommRing α] :
Lean.Grind.CommRing α
Equations

- CommRing.toGrindCommRing α = { toRing := Ring.toGrindRing α, mul_comm := ⋯ }

source
theorem Semiring.toGrindSemiring_ofNat (α : Type u_1) [Semiring α] (n : ℕ) :
OfNat.ofNat n = ↑n