mathlib3 documentation

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

The additive equivalence between ulift α and α.

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

The multiplicative equivalence between ulift α and α.

Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.semigroup {α : Type u} [semigroup α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.add_monoid {α : Type u} [add_monoid α] :
Equations
@[protected, instance]
def ulift.monoid {α : Type u} [monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.comm_monoid {α : Type u} [comm_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.add_group {α : Type u} [add_group α] :
Equations
@[protected, instance]
def ulift.group {α : Type u} [group α] :
Equations
@[protected, instance]
def ulift.comm_group {α : Type u} [comm_group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.nontrivial {α : Type u} [nontrivial α] :