Documentation

Mathlib.Algebra.Ring.GrindInstances

Instances for grind. #

source
@[instance 100]
instance Semiring.toGrindSemiring (α : Type u_1) [s : Semiring α] :
Lean.Grind.Semiring α
Equations
    source
    @[instance 100]
    instance CommSemiring.toGrindCommSemiring (α : Type u_1) [s : CommSemiring α] :
    Lean.Grind.CommSemiring α
    Equations
      source
      @[instance 100]
      instance Ring.toGrindRing (α : Type u_1) [s : Ring α] :
      Lean.Grind.Ring α
      Equations
        source
        @[instance 100]
        instance CommRing.toGrindCommRing (α : Type u_1) [s : CommRing α] :
        Lean.Grind.CommRing α
        Equations
          source
          theorem Semiring.toGrindSemiring_ofNat (α : Type u_1) [Semiring α] (n : ℕ) :
          OfNat.ofNat n = ↑n