Instances for grind.

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

Equations

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

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