Documentation

Mathlib.Algebra.Ring.ULift

ULift instances for ring #

This file defines instances for ring, semiring and related structures on ULift types.

(Recall ULift R is just a "copy" of a type R in a higher universe.)

We also provide ULift.ringEquiv : ULift R ≃+* R.

source
instance ULift.mulZeroClass {M₀ : Type u_1} [MulZeroClass M₀] :
MulZeroClass (ULift.{u_2, u_1} M₀)
Equations
    source
    instance ULift.distrib {R : Type u} [Distrib R] :
    Distrib (ULift.{u_1, u} R)
    Equations
      source
      instance ULift.nonUnitalNonAssocSemiring {R : Type u} [NonUnitalNonAssocSemiring R] :
      NonUnitalNonAssocSemiring (ULift.{u_1, u} R)
      Equations
        source
        instance ULift.nonAssocSemiring {R : Type u} [NonAssocSemiring R] :
        NonAssocSemiring (ULift.{u_1, u} R)
        Equations
          source
          instance ULift.nonUnitalSemiring {R : Type u} [NonUnitalSemiring R] :
          NonUnitalSemiring (ULift.{u_1, u} R)
          Equations
            source
            instance ULift.semiring {R : Type u} [Semiring R] :
            Semiring (ULift.{u_1, u} R)
            Equations
              source
              def ULift.ringEquiv {R : Type u} [NonUnitalNonAssocSemiring R] :
              ULift.{u_1, u} R ≃+* R

              The ring equivalence between ULift R and R.

              Equations
                Instances For
                  source
                  instance ULift.nonUnitalCommSemiring {R : Type u} [NonUnitalCommSemiring R] :
                  NonUnitalCommSemiring (ULift.{u_1, u} R)
                  Equations
                    source
                    instance ULift.commSemiring {R : Type u} [CommSemiring R] :
                    CommSemiring (ULift.{u_1, u} R)
                    Equations
                      source
                      instance ULift.nonUnitalNonAssocRing {R : Type u} [NonUnitalNonAssocRing R] :
                      NonUnitalNonAssocRing (ULift.{u_1, u} R)
                      Equations
                        source
                        instance ULift.nonUnitalRing {R : Type u} [NonUnitalRing R] :
                        NonUnitalRing (ULift.{u_1, u} R)
                        Equations
                          source
                          instance ULift.nonAssocRing {R : Type u} [NonAssocRing R] :
                          NonAssocRing (ULift.{u_1, u} R)
                          Equations
                            source
                            instance ULift.ring {R : Type u} [Ring R] :
                            Ring (ULift.{u_1, u} R)
                            Equations
                              source
                              instance ULift.nonUnitalCommRing {R : Type u} [NonUnitalCommRing R] :
                              NonUnitalCommRing (ULift.{u_1, u} R)
                              Equations
                                source
                                instance ULift.commRing {R : Type u} [CommRing R] :
                                CommRing (ULift.{u_1, u} R)
                                Equations