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).
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
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)
The additive equivalence between ULift α
and α
.
Instances For
theorem
AddEquiv.ulift.proof_1
{α : Type u_1}
:
Function.LeftInverse Equiv.ulift.invFun Equiv.ulift.toFun
The multiplicative equivalence between ULift α
and α
.
Instances For
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.addZeroClass.proof_3
{α : Type u_2}
[AddZeroClass α]
:
∀ (x y : ULift.{u_1, u_2} α), ↑Equiv.ulift (x + y) = ↑Equiv.ulift (x + y)
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_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.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
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_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_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)
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_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_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_6
{α : Type u_2}
[AddGroup α]
:
∀ (x : ULift.{u_1, u_2} α) (x_1 : ℕ), ↑Equiv.ulift (x_1 • x) = ↑Equiv.ulift (x_1 • x)
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_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.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)
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.addLeftCancelMonoid.proof_2
{α : Type u_1}
[AddLeftCancelMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
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)
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_3
{α : Type u_2}
[AddRightCancelMonoid α]
:
∀ (x x_1 : ULift.{u_1, u_2} α), ↑Equiv.ulift (x + x_1) = ↑Equiv.ulift (x + x_1)
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
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