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 = Equiv.nonUnitalNonAssocSemiring (equivShrink α).symm

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

Equations

• instNonUnitalSemiringShrink = Equiv.nonUnitalSemiring (equivShrink α).symm

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

Equations

• instAddMonoidWithOneShrink = Equiv.addMonoidWithOne (equivShrink α).symm

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

Equations

• instAddGroupWithOneShrink = Equiv.addGroupWithOne (equivShrink α).symm

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

Equations

• instNonAssocSemiringShrink = Equiv.nonAssocSemiring (equivShrink α).symm

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

Equations

• instSemiringShrink = Equiv.semiring (equivShrink α).symm

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

Equations

• instNonUnitalCommSemiringShrink = Equiv.nonUnitalCommSemiring (equivShrink α).symm

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

Equations

• instCommSemiringShrink = Equiv.commSemiring (equivShrink α).symm

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

Equations

• instNonUnitalNonAssocRingShrink = Equiv.nonUnitalNonAssocRing (equivShrink α).symm

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

Equations

• instNonUnitalRingShrink = Equiv.nonUnitalRing (equivShrink α).symm

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

Equations

• instRingShrink = Equiv.ring (equivShrink α).symm

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

Equations

• instNonUnitalCommRingShrink = Equiv.nonUnitalCommRing (equivShrink α).symm

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

Equations

• instCommRingShrink = Equiv.commRing (equivShrink α).symm

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

Equations

• (_ : Nontrivial (Shrink.{u_2, u_1} α)) = (_ : Nontrivial (Shrink.{u_2, u_1} α))

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

Equations

• instDivisionRingShrink = Equiv.divisionRing (equivShrink α).symm

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

Equations

• instFieldShrink = Equiv.field (equivShrink α).symm