Documentation

Mathlib.Algebra.Ring.Shrink

Transfer ring structures from `α` to `Shrink α` #

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

Instances For

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

NonUnitalNonAssocSemiring (Shrink.{v, u_1} α)

Equations

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

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

NonUnitalSemiring (Shrink.{v, u_1} α)

Equations

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

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

AddMonoidWithOne (Shrink.{v, u_1} α)

Equations

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

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

AddGroupWithOne (Shrink.{v, u_1} α)

Equations

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

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

NonAssocSemiring (Shrink.{v, u_1} α)

Equations

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

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

Semiring (Shrink.{v, u_1} α)

Equations

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

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

NonUnitalCommSemiring (Shrink.{v, u_1} α)

Equations

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

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

CommSemiring (Shrink.{v, u_1} α)

Equations

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

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

NonUnitalNonAssocRing (Shrink.{v, u_1} α)

Equations

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

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

NonUnitalRing (Shrink.{v, u_1} α)

Equations

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

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

NonAssocRing (Shrink.{v, u_1} α)

Equations

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

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

Ring (Shrink.{v, u_1} α)

Equations

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

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

NonUnitalCommRing (Shrink.{v, u_1} α)

Equations

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

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} α)