Transfer field structures from α to Shrink α

@[instance_reducible]

instance Shrink.instNNRatCast {α : Type u_1} [Small.{v, u_1} α] [NNRatCast α] : NNRatCast (Shrink.{v, u_1} α)

Equations

• Shrink.instNNRatCast = (equivShrink α).symm.nnratCast

@[instance_reducible]

instance Shrink.instRatCast {α : Type u_1} [Small.{v, u_1} α] [RatCast α] : RatCast (Shrink.{v, u_1} α)

Equations

• Shrink.instRatCast = (equivShrink α).symm.ratCast

@[instance_reducible]

instance Shrink.instDivisionRing {α : Type u_1} [Small.{v, u_1} α] [DivisionRing α] : DivisionRing (Shrink.{v, u_1} α)

Equations

• Shrink.instDivisionRing = (equivShrink α).symm.divisionRing

@[instance_reducible]

instance Shrink.instField {α : Type u_1} [Small.{v, u_1} α] [Field α] : Field (Shrink.{v, u_1} α)

Equations

• Shrink.instField = (equivShrink α).symm.field