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 α] :

Zero (ULift.{u_2, u} α)

instance ULift.one {α : Type u} [One α] :

One (ULift.{u_2, u} α)

@[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} α)

instance ULift.mul {α : Type u} [Mul α] :

Mul (ULift.{u_2, u} α)

@[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} α)

instance ULift.div {α : Type u} [Div α] :

Div (ULift.{u_2, u} α)

@[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} α)

instance ULift.inv {α : Type u} [Inv α] :

Inv (ULift.{u_2, u} α)

@[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} β)

instance ULift.smul {α : Type u} {β : Type u_1} [SMul α β] :

SMul α (ULift.{u_2, u_1} β)

@[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} α) β

@[simp]

theorem ULift.pow_down {α : Type u} {β : Type u_1} [Pow α β] (a : ULift.{v, u} α) (b : β) :

(a ^ b).down = a.down ^ b

theorem AddEquiv.ulift.proof_2 {α : Type u_1} :

Function.RightInverse Equiv.ulift.invFun Equiv.ulift.toFun

theorem AddEquiv.ulift.proof_3 {α : Type u_2} [Add α] :

∀ (x x_1 : ULift.{u_1, u_2} α), Equiv.toFun { toFun := Equiv.ulift.toFun, invFun := Equiv.ulift.invFun, left_inv := (_ : Function.LeftInverse Equiv.ulift.invFun Equiv.ulift.toFun), right_inv := (_ : Function.RightInverse Equiv.ulift.invFun Equiv.ulift.toFun) } (x + x_1) = Equiv.toFun { toFun := Equiv.ulift.toFun, invFun := Equiv.ulift.invFun, left_inv := (_ : Function.LeftInverse Equiv.ulift.invFun Equiv.ulift.toFun), right_inv := (_ : Function.RightInverse Equiv.ulift.invFun Equiv.ulift.toFun) } (x + x_1)

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

ULift.{u_2, u} α ≃+ α

The additive equivalence between ULift α and α.

Instances For

theorem AddEquiv.ulift.proof_1 {α : Type u_1} :

Function.LeftInverse Equiv.ulift.invFun Equiv.ulift.toFun

def MulEquiv.ulift {α : Type u} [Mul α] :

ULift.{u_2, u} α ≃* α

The multiplicative equivalence between ULift α and α.

Instances For

instance ULift.semigroup {α : Type u} [Semigroup α] :

Semigroup (ULift.{u_2, u} α)

instance ULift.addSemigroup {α : Type u} [AddSemigroup α] :

AddSemigroup (ULift.{u_2, u} α)

theorem ULift.addCommSemigroup.proof_1 {α : Type u_1} :

Function.Injective ↑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)

instance ULift.addCommSemigroup {α : Type u} [AddCommSemigroup α] :

AddCommSemigroup (ULift.{u_2, u} α)

instance ULift.commSemigroup {α : Type u} [CommSemigroup α] :

CommSemigroup (ULift.{u_2, u} α)

instance ULift.addZeroClass {α : Type u} [AddZeroClass α] :

AddZeroClass (ULift.{u_2, u} α)

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)

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} α)

instance ULift.mulZeroOneClass {α : Type u} [MulZeroOneClass α] :

MulZeroOneClass (ULift.{u_2, u} α)

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_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

instance ULift.addMonoid {α : Type u} [AddMonoid α] :

AddMonoid (ULift.{u_2, u} α)

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_2 {α : Type u_1} [AddMonoid α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

instance ULift.monoid {α : Type u} [Monoid α] :

Monoid (ULift.{u_2, u} α)

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_2 {α : Type u_1} [AddCommMonoid α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

instance ULift.addCommMonoid {α : Type u} [AddCommMonoid α] :

AddCommMonoid (ULift.{u_2, u} α)

theorem ULift.addCommMonoid.proof_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

instance ULift.commMonoid {α : Type u} [CommMonoid α] :

CommMonoid (ULift.{u_2, u} α)

instance ULift.natCast {α : Type u} [NatCast α] :

NatCast (ULift.{u_2, u} α)

instance ULift.intCast {α : Type u} [IntCast α] :

IntCast (ULift.{u_2, u} α)

@[simp]

theorem ULift.up_natCast {α : Type u} [NatCast α] (n : ℕ) :

{ down := ↑n } = ↑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_intCast {α : Type u} [IntCast α] (n : ℤ) :

(↑n).down = ↑n

instance ULift.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :

AddMonoidWithOne (ULift.{u_2, u} α)

instance ULift.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :

AddCommMonoidWithOne (ULift.{u_2, u} α)

instance ULift.monoidWithZero {α : Type u} [MonoidWithZero α] :

MonoidWithZero (ULift.{u_2, u} α)

instance ULift.commMonoidWithZero {α : Type u} [CommMonoidWithZero α] :

CommMonoidWithZero (ULift.{u_2, u} α)

theorem ULift.subNegAddMonoid.proof_2 {α : Type u_1} [SubNegMonoid α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

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_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)

instance ULift.subNegAddMonoid {α : Type u} [SubNegMonoid α] :

SubNegMonoid (ULift.{u_2, u} α)

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_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} α)

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_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_4 {α : Type u_2} [AddGroup α] :

∀ (x : ULift.{u_1, u_2} α), ↑Equiv.ulift (-x) = ↑Equiv.ulift (-x)

theorem ULift.addGroup.proof_2 {α : Type u_1} [AddGroup α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

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)

instance ULift.addGroup {α : Type u} [AddGroup α] :

AddGroup (ULift.{u_2, u} α)

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.group {α : Type u} [Group α] :

Group (ULift.{u_2, u} α)

theorem ULift.addCommGroup.proof_2 {α : Type u_1} [AddCommGroup α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

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_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_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_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_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

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)

instance ULift.addCommGroup {α : Type u} [AddCommGroup α] :

AddCommGroup (ULift.{u_2, u} α)

instance ULift.commGroup {α : Type u} [CommGroup α] :

CommGroup (ULift.{u_2, u} α)

instance ULift.addGroupWithOne {α : Type u} [AddGroupWithOne α] :

AddGroupWithOne (ULift.{u_2, u} α)

instance ULift.addCommGroupWithOne {α : Type u} [AddCommGroupWithOne α] :

AddCommGroupWithOne (ULift.{u_2, u} α)

instance ULift.groupWithZero {α : Type u} [GroupWithZero α] :

GroupWithZero (ULift.{u_2, u} α)

instance ULift.commGroupWithZero {α : Type u} [CommGroupWithZero α] :

CommGroupWithZero (ULift.{u_2, u} α)

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.addLeftCancelSemigroup {α : Type u} [AddLeftCancelSemigroup α] :

AddLeftCancelSemigroup (ULift.{u_2, u} α)

instance ULift.leftCancelSemigroup {α : Type u} [LeftCancelSemigroup α] :

LeftCancelSemigroup (ULift.{u_2, u} α)

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)

theorem ULift.addRightCancelSemigroup.proof_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

instance ULift.addRightCancelSemigroup {α : Type u} [AddRightCancelSemigroup α] :

AddRightCancelSemigroup (ULift.{u_2, u} α)

instance ULift.rightCancelSemigroup {α : Type u} [RightCancelSemigroup α] :

RightCancelSemigroup (ULift.{u_2, u} α)

theorem ULift.addLeftCancelMonoid.proof_2 {α : Type u_1} [AddLeftCancelMonoid α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

theorem ULift.addLeftCancelMonoid.proof_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

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)

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)

instance ULift.addLeftCancelMonoid {α : Type u} [AddLeftCancelMonoid α] :

AddLeftCancelMonoid (ULift.{u_2, u} α)

instance ULift.leftCancelMonoid {α : Type u} [LeftCancelMonoid α] :

LeftCancelMonoid (ULift.{u_2, u} α)

instance ULift.addRightCancelMonoid {α : Type u} [AddRightCancelMonoid α] :

AddRightCancelMonoid (ULift.{u_2, u} α)

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)

theorem ULift.addRightCancelMonoid.proof_2 {α : Type u_1} [AddRightCancelMonoid α] :

↑Equiv.ulift 0 = ↑Equiv.ulift 0

theorem ULift.addRightCancelMonoid.proof_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

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} α)

theorem ULift.addCancelMonoid.proof_1 {α : Type u_1} :

Function.Injective ↑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_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.addCancelMonoid {α : Type u} [AddCancelMonoid α] :

AddCancelMonoid (ULift.{u_2, u} α)

instance ULift.cancelMonoid {α : Type u} [CancelMonoid α] :

CancelMonoid (ULift.{u_2, u} α)

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

instance ULift.addCancelCommMonoid {α : Type u} [AddCancelCommMonoid α] :

AddCancelCommMonoid (ULift.{u_2, u} α)

theorem ULift.addCancelCommMonoid.proof_1 {α : Type u_1} :

Function.Injective ↑Equiv.ulift

instance ULift.cancelCommMonoid {α : Type u} [CancelCommMonoid α] :

CancelCommMonoid (ULift.{u_2, u} α)

instance ULift.nontrivial {α : Type u} [Nontrivial α] :

Nontrivial (ULift.{u_2, u} α)