# mathlibdocumentation

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 use tactic.pi_instance_derive_field, even though it wasn't intended for this purpose, which seems to work fine.

We also provide ulift.mul_equiv : ulift R ≃* R (and its additive analogue).

@[instance]
def ulift.has_zero {α : Type u} [has_zero α] :

@[instance]
def ulift.has_one {α : Type u} [has_one α] :

Equations
@[simp]
theorem ulift.one_down {α : Type u} [has_one α] :
1.down = 1

@[simp]
theorem ulift.zero_down {α : Type u} [has_zero α] :
0.down = 0

@[instance]

@[instance]
def ulift.has_mul {α : Type u} [has_mul α] :

Equations
@[simp]
theorem ulift.mul_down {α : Type u} {x y : ulift α} [has_mul α] :
(x * y).down = (x.down) * y.down

@[simp]
theorem ulift.add_down {α : Type u} {x y : ulift α} [has_add α] :
(x + y).down = x.down + y.down

@[instance]
def ulift.has_div {α : Type u} [has_div α] :

Equations
@[instance]
def ulift.has_sub {α : Type u} [has_sub α] :

@[simp]
theorem ulift.sub_down {α : Type u} {x y : ulift α} [has_sub α] :
(x - y).down = x.down - y.down

@[simp]
theorem ulift.div_down {α : Type u} {x y : ulift α} [has_div α] :
(x / y).down = x.down / y.down

@[instance]
def ulift.has_neg {α : Type u} [has_neg α] :

@[instance]
def ulift.has_inv {α : Type u} [has_inv α] :

Equations
@[simp]
theorem ulift.inv_down {α : Type u} {x : ulift α} [has_inv α] :

@[simp]
theorem ulift.neg_down {α : Type u} {x : ulift α} [has_neg α] :
(-x).down = -x.down

@[instance]
def ulift.add_semigroup {α : Type u}  :

@[instance]
def ulift.semigroup {α : Type u} [semigroup α] :

Equations
def ulift.mul_equiv {α : Type u} [semigroup α] :
≃* α

The multiplicative equivalence between ulift α and α.

Equations
def ulift.add_equiv {α : Type u}  :
≃+ α

The additive equivalence between ulift α and α.

@[instance]
def ulift.add_comm_semigroup {α : Type u}  :

@[instance]
def ulift.comm_semigroup {α : Type u}  :

Equations
@[instance]

@[instance]
def ulift.monoid {α : Type u} [monoid α] :

Equations
@[instance]
def ulift.add_comm_monoid {α : Type u}  :

@[instance]
def ulift.comm_monoid {α : Type u} [comm_monoid α] :

Equations
@[instance]

@[instance]
def ulift.group {α : Type u} [group α] :

Equations
@[instance]
def ulift.comm_group {α : Type u} [comm_group α] :

Equations
@[instance]
def ulift.add_comm_group {α : Type u}  :

@[instance]
def ulift.add_left_cancel_semigroup {α : Type u}  :

@[instance]
def ulift.left_cancel_semigroup {α : Type u}  :

Equations
@[instance]
def ulift.right_cancel_semigroup {α : Type u}  :

Equations
@[instance]
def ulift.add_right_cancel_semigroup {α : Type u}  :