Transfer ring structures from α to Shrink α

noncomputable def Shrink.ringEquiv (α : Type u_1) [Small.{v, u_1} α] [Add α] [Mul α] : Shrink.{v, u_1} α ≃+* α

Shrink α to a smaller universe preserves ring structure.

Equations

• Shrink.ringEquiv α = (equivShrink α).symm.ringEquiv

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalNonAssocSemiring = (equivShrink α).symm.nonUnitalNonAssocSemiring

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalSemiring = (equivShrink α).symm.nonUnitalSemiring

@[implicit_reducible]

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

Equations

• Shrink.instAddMonoidWithOne = (equivShrink α).symm.addMonoidWithOne

@[implicit_reducible]

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

Equations

• Shrink.instAddGroupWithOne = (equivShrink α).symm.addGroupWithOne

@[implicit_reducible]

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

Equations

• Shrink.instNonAssocSemiring = (equivShrink α).symm.nonAssocSemiring

@[implicit_reducible]

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

Equations

• Shrink.instSemiring = (equivShrink α).symm.semiring

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalCommSemiring = (equivShrink α).symm.nonUnitalCommSemiring

@[implicit_reducible]

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

Equations

• Shrink.instCommSemiring = (equivShrink α).symm.commSemiring

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalNonAssocRing = (equivShrink α).symm.nonUnitalNonAssocRing

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalRing = (equivShrink α).symm.nonUnitalRing

@[implicit_reducible]

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

Equations

• Shrink.instNonAssocRing = (equivShrink α).symm.nonAssocRing

@[implicit_reducible]

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

Equations

• Shrink.instRing = (equivShrink α).symm.ring

@[implicit_reducible]

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

Equations

• Shrink.instNonUnitalCommRing = (equivShrink α).symm.nonUnitalCommRing

@[implicit_reducible]

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

Equations

• Shrink.instCommRing = (equivShrink α).symm.commRing

instance Shrink.instIsDomain {α : Type u_1} [Small.{v, u_1} α] [Semiring α] [IsDomain α] : IsDomain (Shrink.{v, u_1} α)