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

ink

instance ULift.zero {α : Type u} [inst : Zero α] : Zero (ULift α)

Equations

• ULift.zero = { zero := { down := 0 } }

ink

instance ULift.one {α : Type u} [inst : One α] : One (ULift α)

Equations

• ULift.one = { one := { down := 1 } }

ink

@[simp]

theorem ULift.zero_down {α : Type u} [inst : Zero α] : 0.down = 0

ink

@[simp]

theorem ULift.one_down {α : Type u} [inst : One α] : 1.down = 1

ink

instance ULift.add {α : Type u} [inst : Add α] : Add (ULift α)

Equations

• ULift.add = { add := fun f g => { down := f.down + g.down } }

ink

instance ULift.mul {α : Type u} [inst : Mul α] : Mul (ULift α)

Equations

• ULift.mul = { mul := fun f g => { down := f.down * g.down } }

ink

@[simp]

theorem ULift.add_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Add α] : (x + y).down = x.down + y.down

ink

@[simp]

theorem ULift.mul_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Mul α] : (x * y).down = x.down * y.down

ink

instance ULift.sub {α : Type u} [inst : Sub α] : Sub (ULift α)

Equations

• ULift.sub = { sub := fun f g => { down := f.down - g.down } }

ink

instance ULift.div {α : Type u} [inst : Div α] : Div (ULift α)

Equations

• ULift.div = { div := fun f g => { down := f.down / g.down } }

ink

@[simp]

theorem ULift.sub_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Sub α] : (x - y).down = x.down - y.down

ink

@[simp]

theorem ULift.div_down {α : Type u} {x : ULift α} {y : ULift α} [inst : Div α] : (x / y).down = x.down / y.down

ink

instance ULift.neg {α : Type u} [inst : Neg α] : Neg (ULift α)

Equations

• ULift.neg = { neg := fun f => { down := -f.down } }

ink

instance ULift.inv {α : Type u} [inst : Inv α] : Inv (ULift α)

Equations

• ULift.inv = { inv := fun f => { down := f.down⁻¹ } }

ink

@[simp]

theorem ULift.neg_down {α : Type u} {x : ULift α} [inst : Neg α] : (-x).down = -x.down

ink

@[simp]

theorem ULift.inv_down {α : Type u} {x : ULift α} [inst : Inv α] : x⁻¹.down = x.down⁻¹

ink

instance ULift.vadd {α : Type u} {β : Type u_1} [inst : VAdd α β] : VAdd α (ULift β)

Equations

• ULift.vadd = { vadd := fun n x => { down := n +ᵥ x.down } }

ink

instance ULift.smul {α : Type u} {β : Type u_1} [inst : SMul α β] : SMul α (ULift β)

Equations

• ULift.smul = { smul := fun n x => { down := n • x.down } }

ink

@[simp]

theorem ULift.vadd_down {α : Type u} {β : Type u_1} [inst : VAdd α β] (a : α) (b : ULift β) : (a +ᵥ b).down = a +ᵥ b.down

ink

@[simp]

theorem ULift.smul_down {α : Type u} {β : Type u_1} [inst : SMul α β] (a : α) (b : ULift β) : (a • b).down = a • b.down

ink

instance ULift.pow {α : Type u} {β : Type u_1} [inst : Pow α β] : Pow (ULift α) β

Equations

• ULift.pow = { pow := fun x n => { down := x.down ^ n } }

ink

@[simp]

theorem ULift.pow_down {α : Type u} {β : Type u_1} [inst : Pow α β] (a : ULift α) (b : β) : (a ^ b).down = a.down ^ b

ink

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.

ink

instance ULift.semigroup {α : Type u} [inst : Semigroup α] : Semigroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addSemigroup {α : Type u} [inst : AddSemigroup α] : AddSemigroup (ULift α)

Equations

• ULift.addSemigroup = Function.Injective.addSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x + x_1) = ↑Equiv.ulift (x + x_1))

ink

def ULift.addCommSemigroup.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

instance ULift.addCommSemigroup {α : Type u} [inst : AddCommSemigroup α] : AddCommSemigroup (ULift α)

Equations

• ULift.addCommSemigroup = Function.Injective.addCommSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x + x_1) = ↑Equiv.ulift (x + x_1))

ink

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

ink

instance ULift.commSemigroup {α : Type u} [inst : CommSemigroup α] : CommSemigroup (ULift α)

Equations

• ULift.commSemigroup = Function.Injective.commSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x * x_1) = ↑Equiv.ulift (x * x_1))

ink

def ULift.addZeroClass.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

instance ULift.addZeroClass {α : Type u} [inst : AddZeroClass α] : AddZeroClass (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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)

ink

instance ULift.mulOneClass {α : Type u} [inst : MulOneClass α] : MulOneClass (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.mulZeroOneClass {α : Type u} [inst : MulZeroOneClass α] : MulZeroOneClass (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

def ULift.addMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

instance ULift.addMonoid {α : Type u} [inst : AddMonoid α] : AddMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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)

ink

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

ink

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

ink

instance ULift.monoid {α : Type u} [inst : Monoid α] : Monoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

def ULift.addCommMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

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

ink

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)

ink

instance ULift.addCommMonoid {α : Type u} [inst : AddCommMonoid α] : AddCommMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.commMonoid {α : Type u} [inst : CommMonoid α] : CommMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.natCast {α : Type u} [inst : NatCast α] : NatCast (ULift α)

Equations

• ULift.natCast = { natCast := fun a => { down := ↑a } }

ink

instance ULift.intCast {α : Type u} [inst : IntCast α] : IntCast (ULift α)

Equations

• ULift.intCast = { intCast := fun a => { down := ↑a } }

ink

@[simp]

theorem ULift.up_natCast {α : Type u} [inst : NatCast α] (n : ℕ) : { down := ↑n } = ↑n

ink

@[simp]

theorem ULift.up_intCast {α : Type u} [inst : IntCast α] (n : ℤ) : { down := ↑n } = ↑n

ink

@[simp]

theorem ULift.down_natCast {α : Type u} [inst : NatCast α] (n : ℕ) : (↑n).down = ↑n

ink

@[simp]

theorem ULift.down_intCast {α : Type u} [inst : IntCast α] (n : ℤ) : (↑n).down = ↑n

ink

instance ULift.addMonoidWithOne {α : Type u} [inst : AddMonoidWithOne α] : AddMonoidWithOne (ULift α)

Equations

• ULift.addMonoidWithOne = let src := ULift.one; let src_1 := ULift.addMonoid; AddMonoidWithOne.mk

ink

instance ULift.addCommMonoidWithOne {α : Type u} [inst : AddCommMonoidWithOne α] : AddCommMonoidWithOne (ULift α)

Equations

• ULift.addCommMonoidWithOne = let src := ULift.addMonoidWithOne; let src_1 := ULift.addCommMonoid; AddCommMonoidWithOne.mk (_ : ∀ (a b : ULift α), a + b = b + a)

ink

instance ULift.monoidWithZero {α : Type u} [inst : MonoidWithZero α] : MonoidWithZero (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.commMonoidWithZero {α : Type u} [inst : CommMonoidWithZero α] : CommMonoidWithZero (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

def ULift.subNegAddMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

instance ULift.subNegAddMonoid {α : Type u} [inst : SubNegMonoid α] : SubNegMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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)

ink

instance ULift.divInvMonoid {α : Type u} [inst : DivInvMonoid α] : DivInvMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

def ULift.addGroup.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

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)

ink

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

ink

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

ink

instance ULift.addGroup {α : Type u} [inst : AddGroup α] : AddGroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

instance ULift.group {α : Type u} [inst : Group α] : Group (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addCommGroup {α : Type u} [inst : AddCommGroup α] : AddCommGroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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)

ink

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

ink

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

ink

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

ink

def ULift.addCommGroup.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

instance ULift.commGroup {α : Type u} [inst : CommGroup α] : CommGroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addGroupWithOne {α : Type u} [inst : AddGroupWithOne α] : AddGroupWithOne (ULift α)

Equations

• ULift.addGroupWithOne = let src := ULift.addMonoidWithOne; let src_1 := ULift.addGroup; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : ULift α), -a + a = 0)

ink

instance ULift.addCommGroupWithOne {α : Type u} [inst : AddCommGroupWithOne α] : AddCommGroupWithOne (ULift α)

Equations

• ULift.addCommGroupWithOne = let src := ULift.addGroupWithOne; let src_1 := ULift.addCommGroup; AddCommGroupWithOne.mk

ink

instance ULift.groupWithZero {α : Type u} [inst : GroupWithZero α] : GroupWithZero (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.commGroupWithZero {α : Type u} [inst : CommGroupWithZero α] : CommGroupWithZero (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addLeftCancelSemigroup {α : Type u} [inst : AddLeftCancelSemigroup α] : AddLeftCancelSemigroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

def ULift.addLeftCancelSemigroup.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

instance ULift.leftCancelSemigroup {α : Type u} [inst : LeftCancelSemigroup α] : LeftCancelSemigroup (ULift α)

Equations

• ULift.leftCancelSemigroup = Function.Injective.leftCancelSemigroup ↑Equiv.ulift (_ : Function.Injective ↑Equiv.ulift) (_ : ∀ (x x_1 : ULift α), ↑Equiv.ulift (x * x_1) = ↑Equiv.ulift (x * x_1))

ink

def ULift.addRightCancelSemigroup.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

instance ULift.addRightCancelSemigroup {α : Type u} [inst : AddRightCancelSemigroup α] : AddRightCancelSemigroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.rightCancelSemigroup {α : Type u} [inst : RightCancelSemigroup α] : RightCancelSemigroup (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addLeftCancelMonoid {α : Type u} [inst : AddLeftCancelMonoid α] : AddLeftCancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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)

ink

def ULift.addLeftCancelMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

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

ink

instance ULift.leftCancelMonoid {α : Type u} [inst : LeftCancelMonoid α] : LeftCancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

def ULift.addRightCancelMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

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)

ink

instance ULift.addRightCancelMonoid {α : Type u} [inst : AddRightCancelMonoid α] : AddRightCancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

instance ULift.rightCancelMonoid {α : Type u} [inst : RightCancelMonoid α] : RightCancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.addCancelMonoid {α : Type u} [inst : AddCancelMonoid α] : AddCancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

def ULift.addCancelMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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)

ink

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

ink

instance ULift.cancelMonoid {α : Type u} [inst : CancelMonoid α] : CancelMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

def ULift.addCancelCommMonoid.proof_1 {α : Type u_1} : Function.Injective ↑Equiv.ulift

Equations

• (_ : Function.Injective ↑Equiv.ulift) = (_ : Function.Injective ↑Equiv.ulift)

ink

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

ink

instance ULift.addCancelCommMonoid {α : Type u} [inst : AddCancelCommMonoid α] : AddCancelCommMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

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)

ink

instance ULift.cancelCommMonoid {α : Type u} [inst : CancelCommMonoid α] : CancelCommMonoid (ULift α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance ULift.nontrivial {α : Type u} [inst : Nontrivial α] : Nontrivial (ULift α)

Equations

• @ULift.nontrivial = @ULift.nontrivial.proof_1