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.instNatCast {R : Type u} [NatCast R] :
      NatCast (ULift.{u_1, u} R)
      Equations
        source
        instance ULift.instIntCast {R : Type u} [IntCast R] :
        IntCast (ULift.{u_1, u} R)
        Equations
          source
          @[simp]
          theorem ULift.up_natCast {R : Type u} [NatCast R] (n : ℕ) :
          { down := ↑n } = ↑n
          source
          @[simp]
          theorem ULift.up_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
          { down := OfNat.ofNat n } = OfNat.ofNat n
          source
          @[simp]
          theorem ULift.up_intCast {R : Type u} [IntCast R] (n : ℤ) :
          { down := ↑n } = ↑n
          source
          @[simp]
          theorem ULift.down_natCast {R : Type u} [NatCast R] (n : ℕ) :
          (↑n).down = ↑n
          source
          @[simp]
          theorem ULift.down_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
          (OfNat.ofNat n).down = OfNat.ofNat n
          source
          @[simp]
          theorem ULift.down_intCast {R : Type u} [IntCast R] (n : ℤ) :
          (↑n).down = ↑n
          source
          instance ULift.addMonoidWithOne {R : Type u} [AddMonoidWithOne R] :
          AddMonoidWithOne (ULift.{u_1, u} R)
          Equations
            source
            instance ULift.addCommMonoidWithOne {R : Type u} [AddCommMonoidWithOne R] :
            AddCommMonoidWithOne (ULift.{u_1, u} R)
            Equations
              source
              instance ULift.addGroupWithOne {R : Type u} [AddGroupWithOne R] :
              AddGroupWithOne (ULift.{u_1, u} R)
              Equations
                source
                instance ULift.addCommGroupWithOne {R : Type u} [AddCommGroupWithOne R] :
                AddCommGroupWithOne (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