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

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.zero {α : Type u} [Zero α] : Zero (ULift.{u_1, u} α)

@[simp]

theorem ULift.one_down {α : Type u} [One α] : down 1 = 1

@[simp]

theorem ULift.zero_down {α : Type u} [Zero α] : down 0 = 0

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.add {α : Type u} [Add α] : Add (ULift.{u_1, u} α)

@[simp]

theorem ULift.mul_down {α : Type u} {x y : ULift.{w, u} α} [Mul α] : (x * y).down = x.down * y.down

@[simp]

theorem ULift.add_down {α : Type u} {x y : ULift.{w, u} α} [Add α] : (x + y).down = x.down + y.down

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.sub {α : Type u} [Sub α] : Sub (ULift.{u_1, u} α)

@[simp]

theorem ULift.div_down {α : Type u} {x y : ULift.{w, u} α} [Div α] : (x / y).down = x.down / y.down

@[simp]

theorem ULift.sub_down {α : Type u} {x y : ULift.{w, u} α} [Sub α] : (x - y).down = x.down - y.down

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.neg {α : Type u} [Neg α] : Neg (ULift.{u_1, u} α)

@[simp]

theorem ULift.inv_down {α : Type u} {x : ULift.{w, u} α} [Inv α] : x⁻¹.down = x.down⁻¹

@[simp]

theorem ULift.neg_down {α : Type u} {x : ULift.{w, u} α} [Neg α] : (-x).down = -x.down

@[implicit_reducible]

instance ULift.pow {α : Type u} {β : Type v} [Pow α β] : Pow (ULift.{u_1, u} α) β

@[implicit_reducible]

instance ULift.vadd {α : Type u} {β : Type v} [VAdd β α] : VAdd β (ULift.{u_1, u} α)

@[implicit_reducible]

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

@[simp]

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

@[simp]

theorem ULift.vadd_down {α : Type u} {β : Type v} [VAdd β α] (a : ULift.{w, u} α) (b : β) : (b +ᵥ a).down = b +ᵥ a.down

@[simp]

theorem ULift.smul_down {α : Type u} {β : Type v} [SMul β α] (a : ULift.{w, u} α) (b : β) : (b • a).down = b • a.down

def MulEquiv.ulift {α : Type u} [Mul α] : ULift.{u_1, u} α ≃* α

The multiplicative equivalence between ULift α and α.

def AddEquiv.ulift {α : Type u} [Add α] : ULift.{u_1, u} α ≃+ α

The additive equivalence between ULift α and α.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.monoid {α : Type u} [Monoid α] : Monoid (ULift.{u_1, u} α)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance ULift.group {α : Type u} [Group α] : Group (ULift.{u_1, u} α)

@[implicit_reducible]

instance ULift.addGroup {α : Type u} [AddGroup α] : AddGroup (ULift.{u_1, u} α)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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