Documentation

Mathlib.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 also provide MulEquiv.ulift : ULift R ≃* R≃* R (and its additive analogue).

instance ULift.zero {α : Type u} [inst : Zero α] :
Zero (ULift α)
Equations
  • ULift.zero = { zero := { down := 0 } }
instance ULift.one {α : Type u} [inst : One α] :
One (ULift α)
Equations
  • ULift.one = { one := { down := 1 } }
@[simp]
theorem ULift.zero_down {α : Type u} [inst : Zero α] :
0.down = 0
@[simp]
theorem ULift.one_down {α : Type u} [inst : One α] :
1.down = 1
instance ULift.add {α : Type u} [inst : Add α] :
Add (ULift α)
Equations
  • ULift.add = { add := fun f g => { down := f.down + g.down } }
instance ULift.mul {α : Type u} [inst : Mul α] :
Mul (ULift α)
Equations
  • ULift.mul = { mul := fun f g => { down := f.down * g.down } }
@[simp]
theorem ULift.add_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Add α] :
(x + y).down = x.down + y.down
@[simp]
theorem ULift.mul_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Mul α] :
(x * y).down = x.down * y.down
instance ULift.sub {α : Type u} [inst : Sub α] :
Sub (ULift α)
Equations
  • ULift.sub = { sub := fun f g => { down := f.down - g.down } }
instance ULift.div {α : Type u} [inst : Div α] :
Div (ULift α)
Equations
  • ULift.div = { div := fun f g => { down := f.down / g.down } }
@[simp]
theorem ULift.sub_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Sub α] :
(x - y).down = x.down - y.down
@[simp]
theorem ULift.div_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Div α] :
(x / y).down = x.down / y.down
instance ULift.neg {α : Type u} [inst : Neg α] :
Neg (ULift α)
Equations
  • ULift.neg = { neg := fun f => { down := -f.down } }
instance ULift.inv {α : Type u} [inst : Inv α] :
Inv (ULift α)
Equations
  • ULift.inv = { inv := fun f => { down := f.down⁻¹ } }
@[simp]
theorem ULift.neg_down {α : Type u} {x : ULift α} [inst : Neg α] :
(-x).down = -x.down
@[simp]
theorem ULift.inv_down {α : Type u} {x : ULift α} [inst : Inv α] :
x⁻¹.down = x.down⁻¹
instance ULift.vadd {α : Type u} {β : Type u_1} [inst : VAdd α β] :
VAdd α (ULift β)
Equations
  • ULift.vadd = { vadd := fun n x => { down := n +ᵥ x.down } }
instance ULift.smul {α : Type u} {β : Type u_1} [inst : SMul α β] :
SMul α (ULift β)
Equations
  • ULift.smul = { smul := fun n x => { down := n x.down } }
@[simp]
theorem ULift.vadd_down {α : Type u} {β : Type u_1} [inst : VAdd α β] (a : α) (b : ULift β) :
(a +ᵥ b).down = a +ᵥ b.down
@[simp]
theorem ULift.smul_down {α : Type u} {β : Type u_1} [inst : SMul α β] (a : α) (b : ULift β) :
(a b).down = a b.down
instance ULift.pow {α : Type u} {β : Type u_1} [inst : Pow α β] :
Pow (ULift α) β
Equations
  • ULift.pow = { pow := fun x n => { down := x.down ^ n } }
@[simp]
theorem ULift.pow_down {α : Type u} {β : Type u_1} [inst : Pow α β] (a : ULift α) (b : β) :
(a ^ b).down = a.down ^ b
def ULift.MulEquiv.ulift {α : Type u} [inst : Mul α] :
ULift α ≃* α

The multiplicative equivalence between ULift α and α.

Equations
  • One or more equations did not get rendered due to their size.
instance ULift.semigroup {α : Type u} [inst : Semigroup α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.addSemigroup {α : Type u} [inst : AddSemigroup α] :
Equations
Equations
Equations
def ULift.addCommSemigroup.proof_2 {α : Type u_2} [inst : AddCommSemigroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
instance ULift.commSemigroup {α : Type u} [inst : CommSemigroup α] :
Equations
def ULift.addZeroClass.proof_1 {α : Type u_1} :
Function.Injective Equiv.ulift
Equations
instance ULift.addZeroClass {α : Type u} [inst : AddZeroClass α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addZeroClass.proof_3 {α : Type u_2} [inst : AddZeroClass α] :
∀ (x y : ULift α), Equiv.ulift (x + y) = Equiv.ulift (x + y)
Equations
  • (_ : Equiv.ulift (x + y) = Equiv.ulift (x + y)) = (_ : Equiv.ulift (x + y) = Equiv.ulift (x + y))
def ULift.addZeroClass.proof_2 {α : Type u_1} [inst : AddZeroClass α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
instance ULift.mulOneClass {α : Type u} [inst : MulOneClass α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.mulZeroOneClass {α : Type u} [inst : MulZeroOneClass α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addMonoid.proof_1 {α : Type u_1} :
Function.Injective Equiv.ulift
Equations
instance ULift.addMonoid {α : Type u} [inst : AddMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addMonoid.proof_2 {α : Type u_1} [inst : AddMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
def ULift.addMonoid.proof_4 {α : Type u_2} [inst : AddMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addMonoid.proof_3 {α : Type u_2} [inst : AddMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
instance ULift.monoid {α : Type u} [inst : Monoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addCommMonoid.proof_1 {α : Type u_1} :
Function.Injective Equiv.ulift
Equations
def ULift.addCommMonoid.proof_3 {α : Type u_2} [inst : AddCommMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
def ULift.addCommMonoid.proof_4 {α : Type u_2} [inst : AddCommMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addCommMonoid.proof_2 {α : Type u_1} [inst : AddCommMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
instance ULift.addCommMonoid {α : Type u} [inst : AddCommMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.commMonoid {α : Type u} [inst : CommMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.natCast {α : Type u} [inst : NatCast α] :
Equations
  • ULift.natCast = { natCast := fun a => { down := a } }
instance ULift.intCast {α : Type u} [inst : IntCast α] :
Equations
  • ULift.intCast = { intCast := fun a => { down := a } }
@[simp]
theorem ULift.up_natCast {α : Type u} [inst : NatCast α] (n : ) :
{ down := n } = n
@[simp]
theorem ULift.up_intCast {α : Type u} [inst : IntCast α] (n : ) :
{ down := n } = n
@[simp]
theorem ULift.down_natCast {α : Type u} [inst : NatCast α] (n : ) :
(n).down = n
@[simp]
theorem ULift.down_intCast {α : Type u} [inst : IntCast α] (n : ) :
(n).down = n
Equations
  • ULift.addMonoidWithOne = let src := ULift.one; let src_1 := ULift.addMonoid; AddMonoidWithOne.mk
Equations
  • ULift.addCommMonoidWithOne = let src := ULift.addMonoidWithOne; let src_1 := ULift.addCommMonoid; AddCommMonoidWithOne.mk (_ : ∀ (a b : ULift α), a + b = b + a)
instance ULift.monoidWithZero {α : Type u} [inst : MonoidWithZero α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def ULift.subNegAddMonoid.proof_6 {α : Type u_2} [inst : SubNegMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.subNegAddMonoid.proof_7 {α : Type u_2} [inst : SubNegMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.subNegAddMonoid.proof_5 {α : Type u_2} [inst : SubNegMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
Equations
  • (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x)) = (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x))
def ULift.subNegAddMonoid.proof_4 {α : Type u_2} [inst : SubNegMonoid α] :
∀ (x : ULift α), Equiv.ulift (-x) = Equiv.ulift (-x)
Equations
  • (_ : Equiv.ulift (-x) = Equiv.ulift (-x)) = (_ : Equiv.ulift (-x) = Equiv.ulift (-x))
def ULift.subNegAddMonoid.proof_3 {α : Type u_2} [inst : SubNegMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
instance ULift.subNegAddMonoid {α : Type u} [inst : SubNegMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.subNegAddMonoid.proof_2 {α : Type u_1} [inst : SubNegMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
instance ULift.divInvMonoid {α : Type u} [inst : DivInvMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addGroup.proof_5 {α : Type u_2} [inst : AddGroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
Equations
  • (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x)) = (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x))
def ULift.addGroup.proof_1 {α : Type u_1} :
Function.Injective Equiv.ulift
Equations
def ULift.addGroup.proof_3 {α : Type u_2} [inst : AddGroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
def ULift.addGroup.proof_2 {α : Type u_1} [inst : AddGroup α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
def ULift.addGroup.proof_7 {α : Type u_2} [inst : AddGroup α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addGroup.proof_4 {α : Type u_2} [inst : AddGroup α] :
∀ (x : ULift α), Equiv.ulift (-x) = Equiv.ulift (-x)
Equations
  • (_ : Equiv.ulift (-x) = Equiv.ulift (-x)) = (_ : Equiv.ulift (-x) = Equiv.ulift (-x))
instance ULift.addGroup {α : Type u} [inst : AddGroup α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addGroup.proof_6 {α : Type u_2} [inst : AddGroup α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
instance ULift.group {α : Type u} [inst : Group α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.addCommGroup {α : Type u} [inst : AddCommGroup α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addCommGroup.proof_4 {α : Type u_2} [inst : AddCommGroup α] :
∀ (x : ULift α), Equiv.ulift (-x) = Equiv.ulift (-x)
Equations
  • (_ : Equiv.ulift (-x) = Equiv.ulift (-x)) = (_ : Equiv.ulift (-x) = Equiv.ulift (-x))
def ULift.addCommGroup.proof_2 {α : Type u_1} [inst : AddCommGroup α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
def ULift.addCommGroup.proof_7 {α : Type u_2} [inst : AddCommGroup α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addCommGroup.proof_3 {α : Type u_2} [inst : AddCommGroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
def ULift.addCommGroup.proof_6 {α : Type u_2} [inst : AddCommGroup α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addCommGroup.proof_1 {α : Type u_1} :
Function.Injective Equiv.ulift
Equations
def ULift.addCommGroup.proof_5 {α : Type u_2} [inst : AddCommGroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x - x_1) = Equiv.ulift (x - x_1)
Equations
  • (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x)) = (_ : Equiv.ulift (x - x) = Equiv.ulift (x - x))
instance ULift.commGroup {α : Type u} [inst : CommGroup α] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.addGroupWithOne {α : Type u} [inst : AddGroupWithOne α] :
Equations
  • ULift.addGroupWithOne = let src := ULift.addMonoidWithOne; let src_1 := ULift.addGroup; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : ULift α), -a + a = 0)
Equations
  • ULift.addCommGroupWithOne = let src := ULift.addGroupWithOne; let src_1 := ULift.addCommGroup; AddCommGroupWithOne.mk
instance ULift.groupWithZero {α : Type u} [inst : GroupWithZero α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
def ULift.addLeftCancelSemigroup.proof_2 {α : Type u_2} [inst : AddLeftCancelSemigroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
Equations
def ULift.addRightCancelSemigroup.proof_2 {α : Type u_2} [inst : AddRightCancelSemigroup α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addLeftCancelMonoid.proof_2 {α : Type u_1} [inst : AddLeftCancelMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
Equations
def ULift.addLeftCancelMonoid.proof_4 {α : Type u_2} [inst : AddLeftCancelMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addLeftCancelMonoid.proof_3 {α : Type u_2} [inst : AddLeftCancelMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
  • One or more equations did not get rendered due to their size.
Equations
def ULift.addRightCancelMonoid.proof_4 {α : Type u_2} [inst : AddRightCancelMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
def ULift.addRightCancelMonoid.proof_2 {α : Type u_1} [inst : AddRightCancelMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addRightCancelMonoid.proof_3 {α : Type u_2} [inst : AddRightCancelMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.addCancelMonoid {α : Type u} [inst : AddCancelMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addCancelMonoid.proof_3 {α : Type u_2} [inst : AddCancelMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
def ULift.addCancelMonoid.proof_2 {α : Type u_1} [inst : AddCancelMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
def ULift.addCancelMonoid.proof_4 {α : Type u_2} [inst : AddCancelMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
instance ULift.cancelMonoid {α : Type u} [inst : CancelMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addCancelCommMonoid.proof_4 {α : Type u_2} [inst : AddCancelCommMonoid α] :
∀ (x : ULift α) (x_1 : ), Equiv.ulift (x_1 x) = Equiv.ulift (x_1 x)
Equations
  • (_ : Equiv.ulift (x x) = Equiv.ulift (x x)) = (_ : Equiv.ulift (x x) = Equiv.ulift (x x))
Equations
def ULift.addCancelCommMonoid.proof_3 {α : Type u_2} [inst : AddCancelCommMonoid α] :
∀ (x x_1 : ULift α), Equiv.ulift (x + x_1) = Equiv.ulift (x + x_1)
Equations
  • (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x)) = (_ : Equiv.ulift (x + x) = Equiv.ulift (x + x))
Equations
  • One or more equations did not get rendered due to their size.
def ULift.addCancelCommMonoid.proof_2 {α : Type u_1} [inst : AddCancelCommMonoid α] :
Equiv.ulift 0 = Equiv.ulift 0
Equations
  • (_ : Equiv.ulift 0 = Equiv.ulift 0) = (_ : Equiv.ulift 0 = Equiv.ulift 0)
Equations
  • One or more equations did not get rendered due to their size.