Transfer ring structures from α to Shrink α.

instance instNonUnitalNonAssocSemiringShrink {α : Type u_1} [NonUnitalNonAssocSemiring α] [Small.{u_2, u_1} α] : NonUnitalNonAssocSemiring (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalNonAssocSemiringShrink = (equivShrink α).symm.nonUnitalNonAssocSemiring

instance instNonUnitalSemiringShrink {α : Type u_1} [NonUnitalSemiring α] [Small.{u_2, u_1} α] : NonUnitalSemiring (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalSemiringShrink = (equivShrink α).symm.nonUnitalSemiring

instance instAddMonoidWithOneShrink {α : Type u_1} [AddMonoidWithOne α] [Small.{u_2, u_1} α] : AddMonoidWithOne (Shrink.{u_2, u_1} α)

Equations

• instAddMonoidWithOneShrink = (equivShrink α).symm.addMonoidWithOne

instance instAddGroupWithOneShrink {α : Type u_1} [AddGroupWithOne α] [Small.{u_2, u_1} α] : AddGroupWithOne (Shrink.{u_2, u_1} α)

Equations

• instAddGroupWithOneShrink = (equivShrink α).symm.addGroupWithOne

instance instNonAssocSemiringShrink {α : Type u_1} [NonAssocSemiring α] [Small.{u_2, u_1} α] : NonAssocSemiring (Shrink.{u_2, u_1} α)

Equations

• instNonAssocSemiringShrink = (equivShrink α).symm.nonAssocSemiring

instance instSemiringShrink {α : Type u_1} [Semiring α] [Small.{u_2, u_1} α] : Semiring (Shrink.{u_2, u_1} α)

Equations

• instSemiringShrink = (equivShrink α).symm.semiring

instance instNonUnitalCommSemiringShrink {α : Type u_1} [NonUnitalCommSemiring α] [Small.{u_2, u_1} α] : NonUnitalCommSemiring (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalCommSemiringShrink = (equivShrink α).symm.nonUnitalCommSemiring

instance instCommSemiringShrink {α : Type u_1} [CommSemiring α] [Small.{u_2, u_1} α] : CommSemiring (Shrink.{u_2, u_1} α)

Equations

• instCommSemiringShrink = (equivShrink α).symm.commSemiring

instance instNonUnitalNonAssocRingShrink {α : Type u_1} [NonUnitalNonAssocRing α] [Small.{u_2, u_1} α] : NonUnitalNonAssocRing (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalNonAssocRingShrink = (equivShrink α).symm.nonUnitalNonAssocRing

instance instNonUnitalRingShrink {α : Type u_1} [NonUnitalRing α] [Small.{u_2, u_1} α] : NonUnitalRing (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalRingShrink = (equivShrink α).symm.nonUnitalRing

instance instRingShrink {α : Type u_1} [Ring α] [Small.{u_2, u_1} α] : Ring (Shrink.{u_2, u_1} α)

Equations

• instRingShrink = (equivShrink α).symm.ring

instance instNonUnitalCommRingShrink {α : Type u_1} [NonUnitalCommRing α] [Small.{u_2, u_1} α] : NonUnitalCommRing (Shrink.{u_2, u_1} α)

Equations

• instNonUnitalCommRingShrink = (equivShrink α).symm.nonUnitalCommRing

instance instCommRingShrink {α : Type u_1} [CommRing α] [Small.{u_2, u_1} α] : CommRing (Shrink.{u_2, u_1} α)

Equations

• instCommRingShrink = (equivShrink α).symm.commRing

instance instNontrivialShrink {α : Type u_1} [Nontrivial α] [Small.{u_2, u_1} α] : Nontrivial (Shrink.{u_2, u_1} α)

Equations

• ⋯ = ⋯

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

Equations

• instDivisionRingShrink = (equivShrink α).symm.divisionRing

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

Equations

• instFieldShrink = (equivShrink α).symm.field