Transfer field structures from α to Shrink α

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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