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

source
@[protected, instance]
def ulift.has_zero {α : Type u} [has_zero α] :
has_zero (ulift α)
Equations
source
@[protected, instance]
def ulift.has_one {α : Type u} [has_one α] :
has_one (ulift α)
Equations
source
@[simp]
theorem ulift.one_down {α : Type u} [has_one α] :
1.down = 1
source
@[simp]
theorem ulift.zero_down {α : Type u} [has_zero α] :
0.down = 0
source
@[protected, instance]
def ulift.has_add {α : Type u} [has_add α] :
has_add (ulift α)
Equations
source
@[protected, instance]
def ulift.has_mul {α : Type u} [has_mul α] :
has_mul (ulift α)
Equations
source
@[simp]
theorem ulift.mul_down {α : Type u} {x y : ulift α} [has_mul α] :
(x * y).down = x.down * y.down
source
@[simp]
theorem ulift.add_down {α : Type u} {x y : ulift α} [has_add α] :
(x + y).down = x.down + y.down
source
@[protected, instance]
def ulift.has_div {α : Type u} [has_div α] :
has_div (ulift α)
Equations
source
@[protected, instance]
def ulift.has_sub {α : Type u} [has_sub α] :
has_sub (ulift α)
Equations
source
@[simp]
theorem ulift.sub_down {α : Type u} {x y : ulift α} [has_sub α] :
(x - y).down = x.down - y.down
source
@[simp]
theorem ulift.div_down {α : Type u} {x y : ulift α} [has_div α] :
(x / y).down = x.down / y.down
source
@[protected, instance]
def ulift.has_neg {α : Type u} [has_neg α] :
has_neg (ulift α)
Equations
source
@[protected, instance]
def ulift.has_inv {α : Type u} [has_inv α] :
has_inv (ulift α)
Equations
source
@[simp]
theorem ulift.inv_down {α : Type u} {x : ulift α} [has_inv α] :
x⁻¹.down = (x.down)⁻¹
source
@[simp]
theorem ulift.neg_down {α : Type u} {x : ulift α} [has_neg α] :
(-x).down = -x.down
source
@[protected, instance]
def ulift.has_smul {α : Type u} {β : Type u_1} [has_smul α β] :
has_smul α (ulift β)
Equations
source
@[protected, instance]
def ulift.has_vadd {α : Type u} {β : Type u_1} [has_vadd α β] :
has_vadd α (ulift β)
Equations
source
@[simp]
theorem ulift.smul_down {α : Type u} {β : Type u_1} [has_smul α β] (a : α) (b : ulift β) :
(a • b).down = a • b.down
source
@[simp]
theorem ulift.vadd_down {α : Type u} {β : Type u_1} [has_vadd α β] (a : α) (b : ulift β) :
(a +ᵥ b).down = a +ᵥ b.down
source
@[protected, instance]
def ulift.has_pow {α : Type u} {β : Type u_1} [has_pow α β] :
has_pow (ulift α) β
Equations
source
@[simp]
theorem ulift.pow_down {α : Type u} {β : Type u_1} [has_pow α β] (a : ulift α) (b : β) :
(a ^ b).down = a.down ^ b
source
def add_equiv.ulift {α : Type u} [has_add α] :
ulift α ≃+ α

The additive equivalence between ulift α and α.

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

The multiplicative equivalence between ulift α and α.

Equations
source
@[protected, instance]
def ulift.add_semigroup {α : Type u} [add_semigroup α] :
add_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.semigroup {α : Type u} [semigroup α] :
semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :
add_comm_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.comm_semigroup {α : Type u} [comm_semigroup α] :
comm_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.mul_one_class {α : Type u} [mul_one_class α] :
mul_one_class (ulift α)
Equations
source
@[protected, instance]
def ulift.add_zero_class {α : Type u} [add_zero_class α] :
add_zero_class (ulift α)
Equations
source
@[protected, instance]
def ulift.mul_zero_one_class {α : Type u} [mul_zero_one_class α] :
mul_zero_one_class (ulift α)
Equations
source
@[protected, instance]
def ulift.add_monoid {α : Type u} [add_monoid α] :
add_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.monoid {α : Type u} [monoid α] :
monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_comm_monoid {α : Type u} [add_comm_monoid α] :
add_comm_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.comm_monoid {α : Type u} [comm_monoid α] :
comm_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.has_nat_cast {α : Type u} [has_nat_cast α] :
has_nat_cast (ulift α)
Equations
source
@[protected, instance]
def ulift.has_int_cast {α : Type u} [has_int_cast α] :
has_int_cast (ulift α)
Equations
source
@[simp, norm_cast]
theorem ulift.up_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
{down := ↑n} = ↑n
source
@[simp, norm_cast]
theorem ulift.up_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
{down := ↑n} = ↑n
source
@[simp, norm_cast]
theorem ulift.down_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
↑n.down = ↑n
source
@[simp, norm_cast]
theorem ulift.down_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
↑n.down = ↑n
source
@[protected, instance]
def ulift.add_monoid_with_one {α : Type u} [add_monoid_with_one α] :
add_monoid_with_one (ulift α)
Equations
source
@[protected, instance]
def ulift.add_comm_monoid_with_one {α : Type u} [add_comm_monoid_with_one α] :
add_comm_monoid_with_one (ulift α)
Equations
source
@[protected, instance]
def ulift.monoid_with_zero {α : Type u} [monoid_with_zero α] :
monoid_with_zero (ulift α)
Equations
source
@[protected, instance]
def ulift.comm_monoid_with_zero {α : Type u} [comm_monoid_with_zero α] :
comm_monoid_with_zero (ulift α)
Equations
source
@[protected, instance]
def ulift.div_inv_monoid {α : Type u} [div_inv_monoid α] :
div_inv_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.sub_neg_add_monoid {α : Type u} [sub_neg_monoid α] :
sub_neg_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_group {α : Type u} [add_group α] :
add_group (ulift α)
Equations
source
@[protected, instance]
def ulift.group {α : Type u} [group α] :
group (ulift α)
Equations
source
@[protected, instance]
def ulift.comm_group {α : Type u} [comm_group α] :
comm_group (ulift α)
Equations
source
@[protected, instance]
def ulift.add_comm_group {α : Type u} [add_comm_group α] :
add_comm_group (ulift α)
Equations
source
@[protected, instance]
def ulift.add_group_with_one {α : Type u} [add_group_with_one α] :
add_group_with_one (ulift α)
Equations
source
@[protected, instance]
def ulift.add_comm_group_with_one {α : Type u} [add_comm_group_with_one α] :
add_comm_group_with_one (ulift α)
Equations
source
@[protected, instance]
def ulift.group_with_zero {α : Type u} [group_with_zero α] :
group_with_zero (ulift α)
Equations
source
@[protected, instance]
def ulift.comm_group_with_zero {α : Type u} [comm_group_with_zero α] :
comm_group_with_zero (ulift α)
Equations
source
@[protected, instance]
def ulift.add_left_cancel_semigroup {α : Type u} [add_left_cancel_semigroup α] :
add_left_cancel_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.left_cancel_semigroup {α : Type u} [left_cancel_semigroup α] :
left_cancel_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.right_cancel_semigroup {α : Type u} [right_cancel_semigroup α] :
right_cancel_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.add_right_cancel_semigroup {α : Type u} [add_right_cancel_semigroup α] :
add_right_cancel_semigroup (ulift α)
Equations
source
@[protected, instance]
def ulift.left_cancel_monoid {α : Type u} [left_cancel_monoid α] :
left_cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_left_cancel_monoid {α : Type u} [add_left_cancel_monoid α] :
add_left_cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_right_cancel_monoid {α : Type u} [add_right_cancel_monoid α] :
add_right_cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.right_cancel_monoid {α : Type u} [right_cancel_monoid α] :
right_cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.cancel_monoid {α : Type u} [cancel_monoid α] :
cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_cancel_monoid {α : Type u} [add_cancel_monoid α] :
add_cancel_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.add_cancel_comm_monoid {α : Type u} [add_cancel_comm_monoid α] :
add_cancel_comm_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.cancel_comm_monoid {α : Type u} [cancel_comm_monoid α] :
cancel_comm_monoid (ulift α)
Equations
source
@[protected, instance]
def ulift.nontrivial {α : Type u} [nontrivial α] :
nontrivial (ulift α)