# mathlib3documentation

algebra.group.ulift

# ulift instances for groups and monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def ulift.has_zero {α : Type u} [has_zero α] :
Equations
@[protected, 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
@[protected, instance]
Equations
@[protected, 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
@[protected, instance]
def ulift.has_div {α : Type u} [has_div α] :
Equations
@[protected, instance]
def ulift.has_sub {α : Type u} [has_sub α] :
Equations
@[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
@[protected, instance]
def ulift.has_neg {α : Type u} [has_neg α] :
Equations
@[protected, 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
@[protected, instance]
def ulift.has_smul {α : Type u} {β : Type u_1} [ β] :
(ulift β)
Equations
@[protected, instance]
def ulift.has_vadd {α : Type u} {β : Type u_1} [ β] :
(ulift β)
Equations
@[simp]
theorem ulift.smul_down {α : Type u} {β : Type u_1} [ β] (a : α) (b : ulift β) :
(a b).down = a b.down
@[simp]
theorem ulift.vadd_down {α : Type u} {β : Type u_1} [ β] (a : α) (b : ulift β) :
(a +ᵥ b).down = a +ᵥ b.down
@[protected, instance]
def ulift.has_pow {α : Type u} {β : Type u_1} [ β] :
has_pow (ulift α) β
Equations
@[simp]
theorem ulift.pow_down {α : Type u} {β : Type u_1} [ β] (a : ulift α) (b : β) :
(a ^ b).down = a.down ^ b
≃+ α

The additive equivalence between ulift α and α.

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

The multiplicative equivalence between ulift α and α.

Equations
@[protected, instance]
def ulift.add_semigroup {α : Type u}  :
Equations
@[protected, instance]
def ulift.semigroup {α : Type u} [semigroup α] :
Equations
@[protected, instance]
def ulift.add_comm_semigroup {α : Type u}  :
Equations
@[protected, instance]
def ulift.comm_semigroup {α : Type u}  :
Equations
@[protected, instance]
def ulift.mul_one_class {α : Type u}  :
Equations
• ulift.mul_one_class = ulift.mul_one_class._proof_1 ulift.mul_one_class._proof_2 ulift.mul_one_class._proof_3
@[protected, instance]
def ulift.add_zero_class {α : Type u}  :
Equations
@[protected, instance]
def ulift.mul_zero_one_class {α : Type u}  :
Equations
• ulift.mul_zero_one_class = ulift.mul_zero_one_class._proof_1 ulift.mul_zero_one_class._proof_2 ulift.mul_zero_one_class._proof_3 ulift.mul_zero_one_class._proof_4
@[protected, instance]
Equations
@[protected, instance]
def ulift.monoid {α : Type u} [monoid α] :
Equations
• ulift.monoid = ulift.monoid._proof_1 ulift.monoid._proof_2 ulift.monoid._proof_3 ulift.monoid._proof_4
@[protected, instance]
def ulift.add_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
def ulift.comm_monoid {α : Type u} [comm_monoid α] :
Equations
• ulift.comm_monoid = ulift.comm_monoid._proof_1 ulift.comm_monoid._proof_2 ulift.comm_monoid._proof_3 ulift.comm_monoid._proof_4
@[protected, instance]
def ulift.has_nat_cast {α : Type u} [has_nat_cast α] :
Equations
@[protected, instance]
def ulift.has_int_cast {α : Type u} [has_int_cast α] :
Equations
@[simp, norm_cast]
theorem ulift.up_nat_cast {α : Type u} [has_nat_cast α] (n : ) :
{down := n} = n
@[simp, norm_cast]
theorem ulift.up_int_cast {α : Type u} [has_int_cast α] (n : ) :
{down := n} = n
@[simp, norm_cast]
theorem ulift.down_nat_cast {α : Type u} [has_nat_cast α] (n : ) :
@[simp, norm_cast]
theorem ulift.down_int_cast {α : Type u} [has_int_cast α] (n : ) :
@[protected, instance]
def ulift.add_monoid_with_one {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.monoid_with_zero {α : Type u}  :
Equations
• ulift.monoid_with_zero = ulift.monoid_with_zero._proof_1 ulift.monoid_with_zero._proof_2 ulift.monoid_with_zero._proof_3 ulift.monoid_with_zero._proof_4 ulift.monoid_with_zero._proof_5
@[protected, instance]
Equations
• ulift.comm_monoid_with_zero = ulift.comm_monoid_with_zero._proof_1 ulift.comm_monoid_with_zero._proof_2 ulift.comm_monoid_with_zero._proof_3 ulift.comm_monoid_with_zero._proof_4 ulift.comm_monoid_with_zero._proof_5
@[protected, instance]
def ulift.div_inv_monoid {α : Type u}  :
Equations
• ulift.div_inv_monoid = ulift.div_inv_monoid._proof_1 ulift.div_inv_monoid._proof_2 ulift.div_inv_monoid._proof_3 ulift.div_inv_monoid._proof_4 ulift.div_inv_monoid._proof_5 ulift.div_inv_monoid._proof_6 ulift.div_inv_monoid._proof_7
@[protected, instance]
def ulift.sub_neg_add_monoid {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.group {α : Type u} [group α] :
Equations
• ulift.group = ulift.group._proof_1 ulift.group._proof_2 ulift.group._proof_3 ulift.group._proof_4 ulift.group._proof_5 ulift.group._proof_6 ulift.group._proof_7
@[protected, instance]
def ulift.comm_group {α : Type u} [comm_group α] :
Equations
• ulift.comm_group = ulift.comm_group._proof_1 ulift.comm_group._proof_2 ulift.comm_group._proof_3 ulift.comm_group._proof_4 ulift.comm_group._proof_5 ulift.comm_group._proof_6 ulift.comm_group._proof_7
@[protected, instance]
def ulift.add_comm_group {α : Type u}  :
Equations
@[protected, instance]
def ulift.add_group_with_one {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.group_with_zero {α : Type u}  :
Equations
• ulift.group_with_zero = ulift.group_with_zero._proof_1 ulift.group_with_zero._proof_2 ulift.group_with_zero._proof_3 ulift.group_with_zero._proof_4 ulift.group_with_zero._proof_5 ulift.group_with_zero._proof_6 ulift.group_with_zero._proof_7 ulift.group_with_zero._proof_8
@[protected, instance]
def ulift.comm_group_with_zero {α : Type u}  :
Equations
• ulift.comm_group_with_zero = ulift.comm_group_with_zero._proof_1 ulift.comm_group_with_zero._proof_2 ulift.comm_group_with_zero._proof_3 ulift.comm_group_with_zero._proof_4 ulift.comm_group_with_zero._proof_5 ulift.comm_group_with_zero._proof_6 ulift.comm_group_with_zero._proof_7 ulift.comm_group_with_zero._proof_8
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.left_cancel_monoid {α : Type u}  :
Equations
• ulift.left_cancel_monoid = ulift.left_cancel_monoid._proof_1 ulift.left_cancel_monoid._proof_2 ulift.left_cancel_monoid._proof_3 ulift.left_cancel_monoid._proof_4
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.right_cancel_monoid {α : Type u}  :
Equations
• ulift.right_cancel_monoid = ulift.right_cancel_monoid._proof_1 ulift.right_cancel_monoid._proof_2 ulift.right_cancel_monoid._proof_3 ulift.right_cancel_monoid._proof_4
@[protected, instance]
def ulift.cancel_monoid {α : Type u}  :
Equations
• ulift.cancel_monoid = ulift.cancel_monoid._proof_1 ulift.cancel_monoid._proof_2 ulift.cancel_monoid._proof_3 ulift.cancel_monoid._proof_4
@[protected, instance]
def ulift.add_cancel_monoid {α : Type u}  :
Equations