Documentation

Mathlib.Algebra.Ring.Shrink

Transfer ring structures from α to Shrink α #

source
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.

Instances For
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalNonAssocSemiring {α : Type u_1} [Small.{v, u_1} α] [NonUnitalNonAssocSemiring α] :
    NonUnitalNonAssocSemiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalSemiring {α : Type u_1} [Small.{v, u_1} α] [NonUnitalSemiring α] :
    NonUnitalSemiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instAddMonoidWithOne {α : Type u_1} [Small.{v, u_1} α] [AddMonoidWithOne α] :
    AddMonoidWithOne (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instAddGroupWithOne {α : Type u_1} [Small.{v, u_1} α] [AddGroupWithOne α] :
    AddGroupWithOne (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonAssocSemiring {α : Type u_1} [Small.{v, u_1} α] [NonAssocSemiring α] :
    NonAssocSemiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instSemiring {α : Type u_1} [Small.{v, u_1} α] [Semiring α] :
    Semiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalCommSemiring {α : Type u_1} [Small.{v, u_1} α] [NonUnitalCommSemiring α] :
    NonUnitalCommSemiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instCommSemiring {α : Type u_1} [Small.{v, u_1} α] [CommSemiring α] :
    CommSemiring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalNonAssocRing {α : Type u_1} [Small.{v, u_1} α] [NonUnitalNonAssocRing α] :
    NonUnitalNonAssocRing (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalRing {α : Type u_1} [Small.{v, u_1} α] [NonUnitalRing α] :
    NonUnitalRing (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonAssocRing {α : Type u_1} [Small.{v, u_1} α] [NonAssocRing α] :
    NonAssocRing (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instRing {α : Type u_1} [Small.{v, u_1} α] [Ring α] :
    Ring (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instNonUnitalCommRing {α : Type u_1} [Small.{v, u_1} α] [NonUnitalCommRing α] :
    NonUnitalCommRing (Shrink.{v, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance Shrink.instCommRing {α : Type u_1} [Small.{v, u_1} α] [CommRing α] :
    CommRing (Shrink.{v, u_1} α)
    source
    instance Shrink.instIsDomain {α : Type u_1} [Small.{v, u_1} α] [Semiring α] [IsDomain α] :
    IsDomain (Shrink.{v, u_1} α)