Documentation

Mathlib.Algebra.Ring.GrindInstances

Instances for grind. #

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