Documentation

Mathlib.Algebra.Group.ULift

ULift instances for groups and monoids #

This file defines instances for group, monoid, semigroup and related structures on ULift types.

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

We also provide MulEquiv.ulift : ULift R ≃* R (and its additive analogue).

instance ULift.one {α : Type u} [One α] :
Equations
    instance ULift.zero {α : Type u} [Zero α] :
    Equations
      @[simp]
      theorem ULift.one_down {α : Type u} [One α] :
      down 1 = 1
      @[simp]
      theorem ULift.zero_down {α : Type u} [Zero α] :
      down 0 = 0
      instance ULift.mul {α : Type u} [Mul α] :
      Equations
        instance ULift.add {α : Type u} [Add α] :
        Equations
          @[simp]
          theorem ULift.mul_down {α : Type u} {x y : ULift.{w, u} α} [Mul α] :
          (x * y).down = x.down * y.down
          @[simp]
          theorem ULift.add_down {α : Type u} {x y : ULift.{w, u} α} [Add α] :
          (x + y).down = x.down + y.down
          instance ULift.div {α : Type u} [Div α] :
          Equations
            instance ULift.sub {α : Type u} [Sub α] :
            Equations
              @[simp]
              theorem ULift.div_down {α : Type u} {x y : ULift.{w, u} α} [Div α] :
              (x / y).down = x.down / y.down
              @[simp]
              theorem ULift.sub_down {α : Type u} {x y : ULift.{w, u} α} [Sub α] :
              (x - y).down = x.down - y.down
              instance ULift.inv {α : Type u} [Inv α] :
              Equations
                instance ULift.neg {α : Type u} [Neg α] :
                Equations
                  @[simp]
                  theorem ULift.inv_down {α : Type u} {x : ULift.{w, u} α} [Inv α] :
                  @[simp]
                  theorem ULift.neg_down {α : Type u} {x : ULift.{w, u} α} [Neg α] :
                  (-x).down = -x.down
                  instance ULift.smul {α : Type u} {β : Type v} [SMul α β] :
                  Equations
                    instance ULift.vadd {α : Type u} {β : Type v} [VAdd α β] :
                    Equations
                      @[simp]
                      theorem ULift.smul_down {α : Type u} {β : Type v} [SMul α β] (a : α) (b : ULift.{w, v} β) :
                      (a b).down = a b.down
                      @[simp]
                      theorem ULift.vadd_down {α : Type u} {β : Type v} [VAdd α β] (a : α) (b : ULift.{w, v} β) :
                      (a +ᵥ b).down = a +ᵥ b.down
                      instance ULift.pow {α : Type u} {β : Type v} [Pow α β] :
                      Equations
                        @[simp]
                        theorem ULift.pow_down {α : Type u} {β : Type v} [Pow α β] (a : ULift.{w, u} α) (b : β) :
                        (a ^ b).down = a.down ^ b
                        def MulEquiv.ulift {α : Type u} [Mul α] :

                        The multiplicative equivalence between ULift α and α.

                        Equations
                          Instances For
                            def AddEquiv.ulift {α : Type u} [Add α] :

                            The additive equivalence between ULift α and α.

                            Equations
                              Instances For
                                Equations
                                  Equations
                                    instance ULift.monoid {α : Type u} [Monoid α] :
                                    Equations
                                      Equations
                                        Equations
                                          instance ULift.instNatCast {α : Type u} [NatCast α] :
                                          Equations
                                            instance ULift.instIntCast {α : Type u} [IntCast α] :
                                            Equations
                                              @[simp]
                                              theorem ULift.up_natCast {α : Type u} [NatCast α] (n : ) :
                                              { down := n } = n
                                              @[simp]
                                              theorem ULift.up_ofNat {α : Type u} [NatCast α] (n : ) [n.AtLeastTwo] :
                                              @[simp]
                                              theorem ULift.up_intCast {α : Type u} [IntCast α] (n : ) :
                                              { down := n } = n
                                              @[simp]
                                              theorem ULift.down_natCast {α : Type u} [NatCast α] (n : ) :
                                              (↑n).down = n
                                              @[simp]
                                              theorem ULift.down_ofNat {α : Type u} [NatCast α] (n : ) [n.AtLeastTwo] :
                                              @[simp]
                                              theorem ULift.down_intCast {α : Type u} [IntCast α] (n : ) :
                                              (↑n).down = n
                                              instance ULift.group {α : Type u} [Group α] :
                                              Equations
                                                instance ULift.addGroup {α : Type u} [AddGroup α] :
                                                Equations
                                                  Equations