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.zero {α : Type u} [Zero α] :
Equations
  • ULift.zero = { zero := { down := 0 } }
instance ULift.one {α : Type u} [One α] :
Equations
  • ULift.one = { one := { down := 1 } }
@[simp]
theorem ULift.zero_down {α : Type u} [Zero α] :
0.down = 0
@[simp]
theorem ULift.one_down {α : Type u} [One α] :
1.down = 1
instance ULift.add {α : Type u} [Add α] :
Equations
  • ULift.add = { add := fun (f g : ULift.{u_2, u} α) => { down := f.down + g.down } }
instance ULift.mul {α : Type u} [Mul α] :
Equations
  • ULift.mul = { mul := fun (f g : ULift.{u_2, u} α) => { down := f.down * g.down } }
@[simp]
theorem ULift.add_down {α : Type u} {x : ULift.{v, u} α} {y : ULift.{v, u} α} [Add α] :
(x + y).down = x.down + y.down
@[simp]
theorem ULift.mul_down {α : Type u} {x : ULift.{v, u} α} {y : ULift.{v, u} α} [Mul α] :
(x * y).down = x.down * y.down
instance ULift.sub {α : Type u} [Sub α] :
Equations
  • ULift.sub = { sub := fun (f g : ULift.{u_2, u} α) => { down := f.down - g.down } }
instance ULift.div {α : Type u} [Div α] :
Equations
  • ULift.div = { div := fun (f g : ULift.{u_2, u} α) => { down := f.down / g.down } }
@[simp]
theorem ULift.sub_down {α : Type u} {x : ULift.{v, u} α} {y : ULift.{v, u} α} [Sub α] :
(x - y).down = x.down - y.down
@[simp]
theorem ULift.div_down {α : Type u} {x : ULift.{v, u} α} {y : ULift.{v, u} α} [Div α] :
(x / y).down = x.down / y.down
instance ULift.neg {α : Type u} [Neg α] :
Equations
instance ULift.inv {α : Type u} [Inv α] :
Equations
@[simp]
theorem ULift.neg_down {α : Type u} {x : ULift.{v, u} α} [Neg α] :
(-x).down = -x.down
@[simp]
theorem ULift.inv_down {α : Type u} {x : ULift.{v, u} α} [Inv α] :
x⁻¹.down = x.down⁻¹
instance ULift.vadd {α : Type u} {β : Type u_1} [VAdd α β] :
Equations
instance ULift.smul {α : Type u} {β : Type u_1} [SMul α β] :
Equations
@[simp]
theorem ULift.vadd_down {α : Type u} {β : Type u_1} [VAdd α β] (a : α) (b : ULift.{v, u_1} β) :
(a +ᵥ b).down = a +ᵥ b.down
@[simp]
theorem ULift.smul_down {α : Type u} {β : Type u_1} [SMul α β] (a : α) (b : ULift.{v, u_1} β) :
(a b).down = a b.down
instance ULift.pow {α : Type u} {β : Type u_1} [Pow α β] :
Equations
  • ULift.pow = { pow := fun (x : ULift.{u_2, u} α) (n : β) => { down := x.down ^ n } }
@[simp]
theorem ULift.pow_down {α : Type u} {β : Type u_1} [Pow α β] (a : ULift.{v, u} α) (b : β) :
(a ^ b).down = a.down ^ b
def AddEquiv.ulift {α : Type u} [Add α] :

The additive equivalence between ULift α and α.

Equations
  • AddEquiv.ulift = let __src := Equiv.ulift; { toEquiv := __src, map_add' := }
Instances For
    theorem AddEquiv.ulift.proof_1 {α : Type u_2} [Add α] :
    ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift.toFun (x + x_1) = Equiv.ulift.toFun (x + x_1)
    def MulEquiv.ulift {α : Type u} [Mul α] :

    The multiplicative equivalence between ULift α and α.

    Equations
    • MulEquiv.ulift = let __src := Equiv.ulift; { toEquiv := __src, map_mul' := }
    Instances For
      Equations
      Equations
      theorem ULift.addCommSemigroup.proof_2 {α : Type u_2} [AddCommSemigroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      Equations
      Equations
      theorem ULift.addZeroClass.proof_1 {α : Type u_1} :
      Function.Injective Equiv.ulift
      theorem ULift.addZeroClass.proof_3 {α : Type u_2} [AddZeroClass α] :
      ∀ (x y : ULift.{u_1, u_2} α), Equiv.ulift (x + y) = Equiv.ulift (x + y)
      Equations
      theorem ULift.addZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      Equations
      Equations
      theorem ULift.addMonoid.proof_3 {α : Type u_2} [AddMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addMonoid.proof_1 {α : Type u_1} :
      Function.Injective Equiv.ulift
      theorem ULift.addMonoid.proof_4 {α : Type u_2} [AddMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addMonoid.proof_2 {α : Type u_1} [AddMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      instance ULift.monoid {α : Type u} [Monoid α] :
      Equations
      theorem ULift.addCommMonoid.proof_2 {α : Type u_1} [AddCommMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      theorem ULift.addCommMonoid.proof_3 {α : Type u_2} [AddCommMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addCommMonoid.proof_4 {α : Type u_2} [AddCommMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addCommMonoid.proof_1 {α : Type u_1} :
      Function.Injective Equiv.ulift
      Equations
      instance ULift.natCast {α : Type u} [NatCast α] :
      Equations
      • ULift.natCast = { natCast := fun (x : ) => { down := x } }
      instance ULift.intCast {α : Type u} [IntCast α] :
      Equations
      • ULift.intCast = { intCast := fun (x : ) => { down := x } }
      @[simp]
      theorem ULift.up_natCast {α : Type u} [NatCast α] (n : ) :
      { down := n } = n
      @[simp]
      theorem ULift.up_ofNat {α : Type u} [NatCast α] (n : ) [Nat.AtLeastTwo n] :
      { down := OfNat.ofNat n } = OfNat.ofNat n
      @[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 : ) [Nat.AtLeastTwo n] :
      @[simp]
      theorem ULift.down_intCast {α : Type u} [IntCast α] (n : ) :
      (n).down = n
      Equations
      • ULift.addMonoidWithOne = let __src := ULift.one; let __src_1 := ULift.addMonoid; AddMonoidWithOne.mk
      Equations
      • ULift.addCommMonoidWithOne = let __src := ULift.addMonoidWithOne; let __src_1 := ULift.addCommMonoid; AddCommMonoidWithOne.mk
      Equations
      Equations
      theorem ULift.subNegAddMonoid.proof_4 {α : Type u_2} [SubNegMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α), Equiv.ulift (-x) = Equiv.ulift (-x)
      theorem ULift.subNegAddMonoid.proof_3 {α : Type u_2} [SubNegMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.subNegAddMonoid.proof_7 {α : Type u_2} [SubNegMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.subNegAddMonoid.proof_2 {α : Type u_1} [SubNegMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      theorem ULift.subNegAddMonoid.proof_6 {α : Type u_2} [SubNegMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.subNegAddMonoid.proof_5 {α : Type u_2} [SubNegMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
      Equations
      theorem ULift.addGroup.proof_7 {α : Type u_2} [AddGroup α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addGroup.proof_2 {α : Type u_1} [AddGroup α] :
      Equiv.ulift 0 = Equiv.ulift 0
      theorem ULift.addGroup.proof_3 {α : Type u_2} [AddGroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addGroup.proof_1 {α : Type u_1} :
      Function.Injective Equiv.ulift
      theorem ULift.addGroup.proof_6 {α : Type u_2} [AddGroup α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      instance ULift.addGroup {α : Type u} [AddGroup α] :
      Equations
      theorem ULift.addGroup.proof_5 {α : Type u_2} [AddGroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
      theorem ULift.addGroup.proof_4 {α : Type u_2} [AddGroup α] :
      ∀ (x : ULift.{u_1, u_2} α), Equiv.ulift (-x) = Equiv.ulift (-x)
      instance ULift.group {α : Type u} [Group α] :
      Equations
      theorem ULift.addCommGroup.proof_6 {α : Type u_2} [AddCommGroup α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addCommGroup.proof_7 {α : Type u_2} [AddCommGroup α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addCommGroup.proof_3 {α : Type u_2} [AddCommGroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addCommGroup.proof_1 {α : Type u_1} :
      Function.Injective Equiv.ulift
      Equations
      theorem ULift.addCommGroup.proof_5 {α : Type u_2} [AddCommGroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
      theorem ULift.addCommGroup.proof_4 {α : Type u_2} [AddCommGroup α] :
      ∀ (x : ULift.{u_1, u_2} α), Equiv.ulift (-x) = Equiv.ulift (-x)
      theorem ULift.addCommGroup.proof_2 {α : Type u_1} [AddCommGroup α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      Equations
      • ULift.addGroupWithOne = let __src := ULift.addMonoidWithOne; let __src_1 := ULift.addGroup; AddGroupWithOne.mk SubNegMonoid.zsmul
      Equations
      • ULift.addCommGroupWithOne = let __src := ULift.addGroupWithOne; let __src_1 := ULift.addCommGroup; AddCommGroupWithOne.mk
      Equations
      Equations
      Equations
      theorem ULift.addLeftCancelSemigroup.proof_2 {α : Type u_2} [AddLeftCancelSemigroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      Equations
      theorem ULift.addRightCancelSemigroup.proof_2 {α : Type u_2} [AddRightCancelSemigroup α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      Equations
      Equations
      Equations
      theorem ULift.addLeftCancelMonoid.proof_2 {α : Type u_1} [AddLeftCancelMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      theorem ULift.addLeftCancelMonoid.proof_3 {α : Type u_2} [AddLeftCancelMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addLeftCancelMonoid.proof_4 {α : Type u_2} [AddLeftCancelMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      Equations
      theorem ULift.addRightCancelMonoid.proof_4 {α : Type u_2} [AddRightCancelMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      Equations
      theorem ULift.addRightCancelMonoid.proof_2 {α : Type u_1} [AddRightCancelMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      theorem ULift.addRightCancelMonoid.proof_3 {α : Type u_2} [AddRightCancelMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      Equations
      Equations
      theorem ULift.addCancelMonoid.proof_3 {α : Type u_2} [AddCancelMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addCancelMonoid.proof_4 {α : Type u_2} [AddCancelMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addCancelMonoid.proof_2 {α : Type u_1} [AddCancelMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      theorem ULift.addCancelCommMonoid.proof_4 {α : Type u_2} [AddCancelCommMonoid α] :
      ∀ (x : ULift.{u_1, u_2} α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
      theorem ULift.addCancelCommMonoid.proof_3 {α : Type u_2} [AddCancelCommMonoid α] :
      ∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
      theorem ULift.addCancelCommMonoid.proof_2 {α : Type u_1} [AddCancelCommMonoid α] :
      Equiv.ulift 0 = Equiv.ulift 0
      Equations
      Equations
      Equations
      • =