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 α] : Zero (ULift.{u_2, u} α)

Equations

• ULift.zero = { zero := { down := 0 } }

instance ULift.one {α : Type u} [One α] : One (ULift.{u_2, u} α)

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 α] : Add (ULift.{u_2, u} α)

Equations

• ULift.add = { add := fun (f g : ULift.{u_2, u} α) => { down := f.down + g.down } }

instance ULift.mul {α : Type u} [Mul α] : Mul (ULift.{u_2, u} α)

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 α] : Sub (ULift.{u_2, u} α)

Equations

• ULift.sub = { sub := fun (f g : ULift.{u_2, u} α) => { down := f.down - g.down } }

instance ULift.div {α : Type u} [Div α] : Div (ULift.{u_2, u} α)

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 α] : Neg (ULift.{u_2, u} α)

Equations

• ULift.neg = { neg := fun (f : ULift.{u_2, u} α) => { down := -f.down } }

instance ULift.inv {α : Type u} [Inv α] : Inv (ULift.{u_2, u} α)

Equations

• ULift.inv = { inv := fun (f : ULift.{u_2, u} α) => { down := f.down⁻¹ } }

@[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 α β] : VAdd α (ULift.{u_2, u_1} β)

Equations

• ULift.vadd = { vadd := fun (n : α) (x : ULift.{u_2, u_1} β) => { down := n +ᵥ x.down } }

instance ULift.smul {α : Type u} {β : Type u_1} [SMul α β] : SMul α (ULift.{u_2, u_1} β)

Equations

• ULift.smul = { smul := fun (n : α) (x : ULift.{u_2, u_1} β) => { down := n • x.down } }

@[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 α β] : Pow (ULift.{u_2, u} α) β

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 α] : ULift.{u_2, u} α ≃+ α

The additive equivalence between ULift α and α.

Equations

• AddEquiv.ulift = let __src := Equiv.ulift; { toEquiv := __src, map_add' := ⋯ }

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 α] : ULift.{u_2, u} α ≃* α

The multiplicative equivalence between ULift α and α.

Equations

• MulEquiv.ulift = let __src := Equiv.ulift; { toEquiv := __src, map_mul' := ⋯ }

instance ULift.semigroup {α : Type u} [Semigroup α] : Semigroup (ULift.{u_2, u} α)

Equations

• ULift.semigroup = Function.Injective.semigroup ⇑MulEquiv.ulift ⋯ ⋯

instance ULift.addSemigroup {α : Type u} [AddSemigroup α] : AddSemigroup (ULift.{u_2, u} α)

Equations

• ULift.addSemigroup = Function.Injective.addSemigroup ⇑Equiv.ulift ⋯ ⋯

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)

theorem ULift.addCommSemigroup.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

instance ULift.addCommSemigroup {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (ULift.{u_2, u} α)

Equations

• ULift.addCommSemigroup = Function.Injective.addCommSemigroup ⇑Equiv.ulift ⋯ ⋯

instance ULift.commSemigroup {α : Type u} [CommSemigroup α] : CommSemigroup (ULift.{u_2, u} α)

Equations

• ULift.commSemigroup = Function.Injective.commSemigroup ⇑Equiv.ulift ⋯ ⋯

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)

instance ULift.addZeroClass {α : Type u} [AddZeroClass α] : AddZeroClass (ULift.{u_2, u} α)

Equations

• ULift.addZeroClass = Function.Injective.addZeroClass ⇑Equiv.ulift ⋯ ⋯ ⋯

theorem ULift.addZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] : Equiv.ulift 0 = Equiv.ulift 0

instance ULift.mulOneClass {α : Type u} [MulOneClass α] : MulOneClass (ULift.{u_2, u} α)

Equations

• ULift.mulOneClass = Function.Injective.mulOneClass ⇑Equiv.ulift ⋯ ⋯ ⋯

instance ULift.mulZeroOneClass {α : Type u} [MulZeroOneClass α] : MulZeroOneClass (ULift.{u_2, u} α)

Equations

• ULift.mulZeroOneClass = Function.Injective.mulZeroOneClass ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.addMonoid {α : Type u} [AddMonoid α] : AddMonoid (ULift.{u_2, u} α)

Equations

• ULift.addMonoid = Function.Injective.addMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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 α] : Monoid (ULift.{u_2, u} α)

Equations

• ULift.monoid = Function.Injective.monoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

theorem ULift.addCommMonoid.proof_2 {α : Type u_1} [AddCommMonoid α] : Equiv.ulift 0 = Equiv.ulift 0

instance ULift.addCommMonoid {α : Type u} [AddCommMonoid α] : AddCommMonoid (ULift.{u_2, u} α)

Equations

• ULift.addCommMonoid = Function.Injective.addCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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

instance ULift.commMonoid {α : Type u} [CommMonoid α] : CommMonoid (ULift.{u_2, u} α)

Equations

• ULift.commMonoid = Function.Injective.commMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.natCast {α : Type u} [NatCast α] : NatCast (ULift.{u_2, u} α)

Equations

• ULift.natCast = { natCast := fun (x : ℕ) => { down := ↑x } }

instance ULift.intCast {α : Type u} [IntCast α] : IntCast (ULift.{u_2, u} α)

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] : (OfNat.ofNat n).down = OfNat.ofNat n

@[simp]

theorem ULift.down_intCast {α : Type u} [IntCast α] (n : ℤ) : (↑n).down = ↑n

instance ULift.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (ULift.{u_2, u} α)

Equations

• ULift.addMonoidWithOne = let __src := ULift.one; let __src_1 := ULift.addMonoid; AddMonoidWithOne.mk ⋯ ⋯

instance ULift.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (ULift.{u_2, u} α)

Equations

• ULift.addCommMonoidWithOne = let __src := ULift.addMonoidWithOne; let __src_1 := ULift.addCommMonoid; AddCommMonoidWithOne.mk ⋯

instance ULift.monoidWithZero {α : Type u} [MonoidWithZero α] : MonoidWithZero (ULift.{u_2, u} α)

Equations

• ULift.monoidWithZero = Function.Injective.monoidWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.commMonoidWithZero {α : Type u} [CommMonoidWithZero α] : CommMonoidWithZero (ULift.{u_2, u} α)

Equations

• ULift.commMonoidWithZero = Function.Injective.commMonoidWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯

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

instance ULift.subNegAddMonoid {α : Type u} [SubNegMonoid α] : SubNegMonoid (ULift.{u_2, u} α)

Equations

• ULift.subNegAddMonoid = Function.Injective.subNegMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

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)

instance ULift.divInvMonoid {α : Type u} [DivInvMonoid α] : DivInvMonoid (ULift.{u_2, u} α)

Equations

• ULift.divInvMonoid = Function.Injective.divInvMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 α] : AddGroup (ULift.{u_2, u} α)

Equations

• ULift.addGroup = Function.Injective.addGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 α] : Group (ULift.{u_2, u} α)

Equations

• ULift.group = Function.Injective.group ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

instance ULift.addCommGroup {α : Type u} [AddCommGroup α] : AddCommGroup (ULift.{u_2, u} α)

Equations

• ULift.addCommGroup = Function.Injective.addCommGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

instance ULift.commGroup {α : Type u} [CommGroup α] : CommGroup (ULift.{u_2, u} α)

Equations

• ULift.commGroup = Function.Injective.commGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.addGroupWithOne {α : Type u} [AddGroupWithOne α] : AddGroupWithOne (ULift.{u_2, u} α)

Equations

• ULift.addGroupWithOne = let __src := ULift.addMonoidWithOne; let __src_1 := ULift.addGroup; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.addCommGroupWithOne {α : Type u} [AddCommGroupWithOne α] : AddCommGroupWithOne (ULift.{u_2, u} α)

Equations

• ULift.addCommGroupWithOne = let __src := ULift.addGroupWithOne; let __src_1 := ULift.addCommGroup; AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

instance ULift.groupWithZero {α : Type u} [GroupWithZero α] : GroupWithZero (ULift.{u_2, u} α)

Equations

• ULift.groupWithZero = Function.Injective.groupWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.commGroupWithZero {α : Type u} [CommGroupWithZero α] : CommGroupWithZero (ULift.{u_2, u} α)

Equations

• ULift.commGroupWithZero = Function.Injective.commGroupWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.addLeftCancelSemigroup {α : Type u} [AddLeftCancelSemigroup α] : AddLeftCancelSemigroup (ULift.{u_2, u} α)

Equations

• ULift.addLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup ⇑Equiv.ulift ⋯ ⋯

theorem ULift.addLeftCancelSemigroup.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

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)

instance ULift.leftCancelSemigroup {α : Type u} [LeftCancelSemigroup α] : LeftCancelSemigroup (ULift.{u_2, u} α)

Equations

• ULift.leftCancelSemigroup = Function.Injective.leftCancelSemigroup ⇑Equiv.ulift ⋯ ⋯

theorem ULift.addRightCancelSemigroup.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

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)

instance ULift.addRightCancelSemigroup {α : Type u} [AddRightCancelSemigroup α] : AddRightCancelSemigroup (ULift.{u_2, u} α)

Equations

• ULift.addRightCancelSemigroup = Function.Injective.addRightCancelSemigroup ⇑Equiv.ulift ⋯ ⋯

instance ULift.rightCancelSemigroup {α : Type u} [RightCancelSemigroup α] : RightCancelSemigroup (ULift.{u_2, u} α)

Equations

• ULift.rightCancelSemigroup = Function.Injective.rightCancelSemigroup ⇑Equiv.ulift ⋯ ⋯

theorem ULift.addLeftCancelMonoid.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

instance ULift.addLeftCancelMonoid {α : Type u} [AddLeftCancelMonoid α] : AddLeftCancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.addLeftCancelMonoid = Function.Injective.addLeftCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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)

instance ULift.leftCancelMonoid {α : Type u} [LeftCancelMonoid α] : LeftCancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.leftCancelMonoid = Function.Injective.leftCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

theorem ULift.addRightCancelMonoid.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

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)

instance ULift.addRightCancelMonoid {α : Type u} [AddRightCancelMonoid α] : AddRightCancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.addRightCancelMonoid = Function.Injective.addRightCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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)

instance ULift.rightCancelMonoid {α : Type u} [RightCancelMonoid α] : RightCancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.rightCancelMonoid = Function.Injective.rightCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.addCancelMonoid {α : Type u} [AddCancelMonoid α] : AddCancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.addCancelMonoid = Function.Injective.addCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

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

instance ULift.cancelMonoid {α : Type u} [CancelMonoid α] : CancelMonoid (ULift.{u_2, u} α)

Equations

• ULift.cancelMonoid = Function.Injective.cancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

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

theorem ULift.addCancelCommMonoid.proof_1 {α : Type u_1} : Function.Injective ⇑Equiv.ulift

instance ULift.addCancelCommMonoid {α : Type u} [AddCancelCommMonoid α] : AddCancelCommMonoid (ULift.{u_2, u} α)

Equations

• ULift.addCancelCommMonoid = Function.Injective.addCancelCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.cancelCommMonoid {α : Type u} [CancelCommMonoid α] : CancelCommMonoid (ULift.{u_2, u} α)

Equations

• ULift.cancelCommMonoid = Function.Injective.cancelCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.nontrivial {α : Type u} [Nontrivial α] : Nontrivial (ULift.{u_2, u} α)

Equations

• ⋯ = ⋯