Documentation

Mathlib.Algebra.Ring.GrindInstances

Instances for grind. #

source
instance CommRing.toGrindCommRing (α : Type u_1) [s : CommRing α] :
Lean.Grind.CommRing α
Equations
    source
    theorem CommRing.toGrindCommRing_ofNat (α : Type u_1) [CommRing α] (n : ℕ) :
    OfNat.ofNat n = ↑n