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≃* R
(and its additive analogue).
Equations
- ULift.addSemigroup = Function.Injective.addSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x + x_1) = ↑Equiv.ulift (x + x_1))
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- ULift.addCommSemigroup = Function.Injective.addCommSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x + x_1) = ↑Equiv.ulift (x + x_1))
Equations
- ULift.commSemigroup = Function.Injective.commSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x * x_1) = ↑Equiv.ulift (x * x_1))
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
def
ULift.addZeroClass.proof_2
{α : Type u_1}
[inst : AddZeroClass α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
def
ULift.addCommMonoid.proof_2
{α : Type u_1}
[inst : AddCommMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ULift.addMonoidWithOne = let src := ULift.one; let src_1 := ULift.addMonoid; AddMonoidWithOne.mk
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
def
ULift.subNegAddMonoid.proof_2
{α : Type u_1}
[inst : SubNegMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
def
ULift.addCommGroup.proof_2
{α : Type u_1}
[inst : AddCommGroup α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- ULift.addCommGroupWithOne = let src := ULift.addGroupWithOne; let src_1 := ULift.addCommGroup; AddCommGroupWithOne.mk
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- ULift.leftCancelSemigroup = Function.Injective.leftCancelSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x * x_1) = ↑Equiv.ulift (x * x_1))
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
def
ULift.addLeftCancelMonoid.proof_2
{α : Type u_1}
[inst : AddLeftCancelMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
def
ULift.addRightCancelMonoid.proof_2
{α : Type u_1}
[inst : AddRightCancelMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
def
ULift.addCancelMonoid.proof_2
{α : Type u_1}
[inst : AddCancelMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)
Equations
- One or more equations did not get rendered due to their size.
def
ULift.addCancelCommMonoid.proof_2
{α : Type u_1}
[inst : AddCancelCommMonoid α]
:
↑Equiv.ulift 0 = ↑Equiv.ulift 0
Equations
- One or more equations did not get rendered due to their size.