Documentation

Mathlib.Algebra.Field.Shrink

Transfer field structures from α to Shrink α #

source
instance Shrink.instNNRatCast {α : Type u_1} [Small.{v, u_1} α] [NNRatCast α] :
NNRatCast (Shrink.{v, u_1} α)
Equations
    source
    instance Shrink.instRatCast {α : Type u_1} [Small.{v, u_1} α] [RatCast α] :
    RatCast (Shrink.{v, u_1} α)
    Equations
      source
      instance Shrink.instDivisionRing {α : Type u_1} [Small.{v, u_1} α] [DivisionRing α] :
      DivisionRing (Shrink.{v, u_1} α)
      Equations
        source
        instance Shrink.instField {α : Type u_1} [Small.{v, u_1} α] [Field α] :
        Field (Shrink.{v, u_1} α)
        Equations