Documentation
Mathlib
.
Algebra
.
Ring
.
GrindInstances
Search
return to top
source
Imports
Init
Mathlib.Algebra.Ring.Defs
Mathlib.Data.Int.Cast.Basic
Imported by
CommRing
.
toGrindCommRing
CommRing
.
toGrindCommRing_ofNat
Instances for
grind
.
#
source
instance
CommRing
.
toGrindCommRing
(
α
:
Type
u_1)
[
s
:
CommRing
α
]
:
Lean.Grind.CommRing
α
Equations
One or more equations did not get rendered due to their size.
source
theorem
CommRing
.
toGrindCommRing_ofNat
(
α
:
Type
u_1)
[
CommRing
α
]
(
n
:
ℕ
)
:
OfNat.ofNat
n
=
↑
n