Instances for grind.

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

@[instance 100]

instance CommSemiring.toGrindCommSemiring (α : Type u_1) [s : CommSemiring α] : Lean.Grind.CommSemiring α

Equations

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

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

@[instance 100]

instance CommRing.toGrindCommRing (α : Type u_1) [s : CommRing α] : Lean.Grind.CommRing α

Equations

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

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