Documentation

Mathlib.Algebra.Ring.Shrink

Transfer ring structures from α to Shrink α #

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