Group structure on the order type synonyms #

Lex.instMonoid = { toSemigroup := Lex.instSemigroup, toOne := Lex.instOne, one_mul := ⋯, mul_one := ⋯, npow := Lex.instMonoid._aux_3, npow_zero := ⋯, npow_succ := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddMonoid {α : Type u_1} [AddMonoid α] :

AddMonoid (Lex α)

Equations

Lex.instAddMonoid = { toAddSemigroup := Lex.instAddSemigroup, toZero := Lex.instZero, zero_add := ⋯, add_zero := ⋯, nsmul := Lex.instAddMonoid._aux_3, nsmul_zero := ⋯, nsmul_succ := ⋯ }

source

@[implicit_reducible]

instance Lex.instCommMonoid {α : Type u_1} [CommMonoid α] :

CommMonoid (Lex α)

Equations

Lex.instCommMonoid = { toMonoid := Lex.instMonoid, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :

AddCommMonoid (Lex α)

Equations

Lex.instAddCommMonoid = { toAddMonoid := Lex.instAddMonoid, add_comm := ⋯ }

source

@[implicit_reducible]

instance Lex.instLeftCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :

LeftCancelMonoid (Lex α)

Equations

Lex.instLeftCancelMonoid = { toMonoid := Lex.instMonoid, toIsLeftCancelMul := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddLeftCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :

AddLeftCancelMonoid (Lex α)

Equations

Lex.instAddLeftCancelMonoid = { toAddMonoid := Lex.instAddMonoid, toIsLeftCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Lex.instRightCancelMonoid {α : Type u_1} [RightCancelMonoid α] :

RightCancelMonoid (Lex α)

Equations

Lex.instRightCancelMonoid = { toMonoid := Lex.instMonoid, toIsRightCancelMul := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddRightCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :

AddRightCancelMonoid (Lex α)

Equations

Lex.instAddRightCancelMonoid = { toAddMonoid := Lex.instAddMonoid, toIsRightCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Lex.instCancelMonoid {α : Type u_1} [CancelMonoid α] :

CancelMonoid (Lex α)

Equations

Lex.instCancelMonoid = { toLeftCancelMonoid := Lex.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :

AddCancelMonoid (Lex α)

Equations

Lex.instAddCancelMonoid = { toAddLeftCancelMonoid := Lex.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Lex.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :

CancelCommMonoid (Lex α)

Equations

Lex.instCancelCommMonoid = { toCommMonoid := Lex.instCommMonoid, toIsLeftCancelMul := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :

AddCancelCommMonoid (Lex α)

Equations

Lex.instAddCancelCommMonoid = { toAddCommMonoid := Lex.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Lex.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :

InvolutiveInv (Lex α)

Equations

Lex.instInvolutiveInv = { toInv := Lex.instInv, inv_inv := ⋯ }

source

@[implicit_reducible]

instance Lex.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :

InvolutiveNeg (Lex α)

Equations

Lex.instInvolutiveNeg = { toNeg := Lex.instNeg, neg_neg := ⋯ }

source

@[implicit_reducible]

instance Lex.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :

DivInvMonoid (Lex α)

Equations

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

source

@[implicit_reducible]

instance Lex.instSubNegAddMonoid {α : Type u_1} [SubNegMonoid α] :

SubNegMonoid (Lex α)

Equations

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

source

@[implicit_reducible]

instance Lex.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :

DivisionMonoid (Lex α)

Equations

Lex.instDivisionMonoid = { toDivInvMonoid := Lex.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

source

@[implicit_reducible]

instance Lex.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :

SubtractionMonoid (Lex α)

Equations

Lex.instSubtractionMonoid = { toSubNegMonoid := Lex.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

source

@[implicit_reducible]

instance Lex.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :

DivisionCommMonoid (Lex α)

Equations

Lex.instDivisionCommMonoid = { toDivisionMonoid := Lex.instDivisionMonoid, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Lex.instDivisionAddCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :

SubtractionCommMonoid (Lex α)

Equations

Lex.instDivisionAddCommMonoid = { toSubtractionMonoid := Lex.instSubtractionMonoid, add_comm := ⋯ }

source

@[implicit_reducible]

instance Lex.instGroup {α : Type u_1} [Group α] :

Group (Lex α)

Equations

Lex.instGroup = { toDivInvMonoid := Lex.instDivInvMonoid, inv_mul_cancel := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddGroup {α : Type u_1} [AddGroup α] :

AddGroup (Lex α)

Equations

Lex.instAddGroup = { toSubNegMonoid := Lex.instSubNegAddMonoid, neg_add_cancel := ⋯ }

source

@[implicit_reducible]

instance Lex.instCommGroup {α : Type u_1} [CommGroup α] :

CommGroup (Lex α)

Equations

Lex.instCommGroup = { toGroup := Lex.instGroup, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Lex.instAddCommGroup {α : Type u_1} [AddCommGroup α] :

AddCommGroup (Lex α)

Equations

Lex.instAddCommGroup = { toAddGroup := Lex.instAddGroup, add_comm := ⋯ }

source

@[simp]

theorem toLex_one {α : Type u_1} [One α] :

toLex 1 = 1

source

@[simp]

theorem toLex_zero {α : Type u_1} [Zero α] :

toLex 0 = 0

source

@[simp]

theorem toLex_eq_one {α : Type u_1} [One α] {a : α} :

toLex a = 1 ↔ a = 1

source

@[simp]

theorem toLex_eq_zero {α : Type u_1} [Zero α] {a : α} :

toLex a = 0 ↔ a = 0

source

@[simp]

theorem ofLex_one {α : Type u_1} [One α] :

ofLex 1 = 1

source

@[simp]

theorem ofLex_zero {α : Type u_1} [Zero α] :

ofLex 0 = 0

source

@[simp]

theorem ofLex_eq_one {α : Type u_1} [One α] {a : Lex α} :

ofLex a = 1 ↔ a = 1

source

@[simp]

theorem ofLex_eq_zero {α : Type u_1} [Zero α] {a : Lex α} :

ofLex a = 0 ↔ a = 0

source

@[simp]

theorem toLex_mul {α : Type u_1} [Mul α] (a b : α) :

toLex (a * b) = toLex a * toLex b

source

@[simp]

theorem toLex_add {α : Type u_1} [Add α] (a b : α) :

toLex (a + b) = toLex a + toLex b

source

@[simp]

theorem ofLex_mul {α : Type u_1} [Mul α] (a b : Lex α) :

ofLex (a * b) = ofLex a * ofLex b

source

@[simp]

theorem ofLex_add {α : Type u_1} [Add α] (a b : Lex α) :

ofLex (a + b) = ofLex a + ofLex b

source

@[simp]

theorem toLex_inv {α : Type u_1} [Inv α] (a : α) :

toLex a⁻¹ = (toLex a)⁻¹

source

@[simp]

theorem toLex_neg {α : Type u_1} [Neg α] (a : α) :

toLex (-a) = -toLex a

source

@[simp]

theorem ofLex_inv {α : Type u_1} [Inv α] (a : Lex α) :

ofLex a⁻¹ = (ofLex a)⁻¹

source

@[simp]

theorem ofLex_neg {α : Type u_1} [Neg α] (a : Lex α) :

ofLex (-a) = -ofLex a

source

@[simp]

theorem toLex_div {α : Type u_1} [Div α] (a b : α) :

toLex (a / b) = toLex a / toLex b

source

@[simp]

theorem toLex_sub {α : Type u_1} [Sub α] (a b : α) :

toLex (a - b) = toLex a - toLex b

source

@[simp]

theorem ofLex_div {α : Type u_1} [Div α] (a b : Lex α) :

ofLex (a / b) = ofLex a / ofLex b

source

@[simp]

theorem ofLex_sub {α : Type u_1} [Sub α] (a b : Lex α) :

ofLex (a - b) = ofLex a - ofLex b

source

@[simp]

theorem toLex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

toLex (a ^ b) = toLex a ^ b

source

@[simp]

theorem toLex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toLex (b • a) = b • toLex a

source

@[simp]

theorem toLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toLex (b +ᵥ a) = b +ᵥ toLex a

source

@[simp]

theorem ofLex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : Lex α) (b : β) :

ofLex (a ^ b) = ofLex a ^ b

source

@[simp]

theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Lex α) :

ofLex (b +ᵥ a) = b +ᵥ ofLex a

source

@[simp]

theorem ofLex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : Lex α) :

ofLex (b • a) = b • ofLex a

source

@[simp]

theorem pow_toLex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

a ^ toLex b = a ^ b

source

@[simp]

theorem toLex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toLex b • a = b • a

source

@[simp]

theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toLex b +ᵥ a = b +ᵥ a

source

@[simp]

theorem pow_ofLex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : Lex β) :

a ^ ofLex b = a ^ b

source

@[simp]

theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : Lex β) (a : α) :

ofLex b +ᵥ a = b +ᵥ a

source

@[simp]

theorem ofLex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Lex β) (a : α) :

ofLex b • a = b • a

source

@[simp]

theorem isLeftRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsLeftRegular (toLex a) ↔ IsLeftRegular a

source

@[simp]

theorem isAddLeftRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddLeftRegular (toLex a) ↔ IsAddLeftRegular a

source

@[simp]

theorem isLeftRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsLeftRegular (ofLex a) ↔ IsLeftRegular a

source

@[simp]

theorem isAddLeftRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddLeftRegular (ofLex a) ↔ IsAddLeftRegular a

source

@[simp]

theorem isRightRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsRightRegular (toLex a) ↔ IsRightRegular a

source

@[simp]

theorem isAddRightRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRightRegular (toLex a) ↔ IsAddRightRegular a

source

@[simp]

theorem isRightRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsRightRegular (ofLex a) ↔ IsRightRegular a

source

@[simp]

theorem isAddRightRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddRightRegular (ofLex a) ↔ IsAddRightRegular a

source

@[simp]

theorem isRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsRegular (toLex a) ↔ IsRegular a

source

@[simp]

theorem isAddRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRegular (toLex a) ↔ IsAddRegular a

source

@[simp]

theorem isRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsRegular (ofLex a) ↔ IsRegular a

source

@[simp]

theorem isAddRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddRegular (ofLex a) ↔ IsAddRegular a

Colexicographical order #

source

@[implicit_reducible]

instance Colex.instOne {α : Type u_1} [One α] :

One (Colex α)

Equations

Colex.instOne = inst✝

source

@[implicit_reducible]

instance Colex.instZero {α : Type u_1} [Zero α] :

Zero (Colex α)

Equations

Colex.instZero = inst✝

source

@[implicit_reducible]

instance Colex.instMul {α : Type u_1} [Mul α] :

Mul (Colex α)

Equations

Colex.instMul = inst✝

source

@[implicit_reducible]

instance Colex.instAdd {α : Type u_1} [Add α] :

Add (Colex α)

Equations

Colex.instAdd = inst✝

source

@[implicit_reducible]

instance Colex.instInv {α : Type u_1} [Inv α] :

Inv (Colex α)

Equations

Colex.instInv = inst✝

source

@[implicit_reducible]

instance Colex.instNeg {α : Type u_1} [Neg α] :

Neg (Colex α)

Equations

Colex.instNeg = inst✝

source

@[implicit_reducible]

instance Colex.instDiv {α : Type u_1} [Div α] :

Div (Colex α)

Equations

Colex.instDiv = inst✝

source

@[implicit_reducible]

instance Colex.instSub {α : Type u_1} [Sub α] :

Sub (Colex α)

Equations

Colex.instSub = inst✝

source

@[implicit_reducible]

instance Colex.instPow {α : Type u_1} {β : Type u_2} [Pow α β] :

Pow (Colex α) β

Equations

Colex.instPow = inst✝

source

@[implicit_reducible]

instance Colex.instSMul {β : Type u_2} {α : Type u_1} [SMul β α] :

SMul β (Colex α)

Equations

Colex.instSMul = inst✝

source

@[implicit_reducible]

instance Colex.instVAdd {β : Type u_2} {α : Type u_1} [VAdd β α] :

VAdd β (Colex α)

Equations

Colex.instVAdd = inst✝

source

@[implicit_reducible]

instance Colex.instPow_1 {α : Type u_1} {β : Type u_2} [Pow α β] :

Pow α (Colex β)

Equations

Colex.instPow_1 = inst✝

source

@[implicit_reducible]

instance Colex.instSMul' {β : Type u_2} {α : Type u_1} [SMul β α] :

SMul (Colex β) α

Equations

Colex.instSMul' = inst✝

source

@[implicit_reducible]

instance Colex.instVAdd' {β : Type u_2} {α : Type u_1} [VAdd β α] :

VAdd (Colex β) α

Equations

Colex.instVAdd' = inst✝

source

@[implicit_reducible]

instance Colex.instSemigroup {α : Type u_1} [Semigroup α] :

Semigroup (Colex α)

Equations

Colex.instSemigroup = { toMul := Colex.instMul, mul_assoc := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddSemigroup {α : Type u_1} [AddSemigroup α] :

AddSemigroup (Colex α)

Equations

Colex.instAddSemigroup = { toAdd := Colex.instAdd, add_assoc := ⋯ }

source

@[implicit_reducible]

instance Colex.instCommSemigroup {α : Type u_1} [CommSemigroup α] :

CommSemigroup (Colex α)

Equations

Colex.instCommSemigroup = { toSemigroup := Colex.instSemigroup, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :

AddCommSemigroup (Colex α)

Equations

Colex.instAddCommSemigroup = { toAddSemigroup := Colex.instAddSemigroup, add_comm := ⋯ }

source

instance Colex.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :

IsLeftCancelMul (Colex α)

source

instance Colex.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :

IsLeftCancelAdd (Colex α)

source

instance Colex.instIsRightCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :

IsRightCancelMul (Colex α)

source

instance Colex.instIsRightCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :

IsRightCancelAdd (Colex α)

source

instance Colex.instIsCancelMul {α : Type u_1} [Mul α] [IsCancelMul α] :

IsCancelMul (Colex α)

source

instance Colex.instIsCancelAdd {α : Type u_1} [Add α] [IsCancelAdd α] :

IsCancelAdd (Colex α)

source

@[implicit_reducible]

instance Colex.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :

LeftCancelSemigroup (Colex α)

Equations

Colex.instLeftCancelSemigroup = { toSemigroup := Colex.instSemigroup, toIsLeftCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :

AddLeftCancelSemigroup (Colex α)

Equations

Colex.instAddLeftCancelSemigroup = { toAddSemigroup := Colex.instAddSemigroup, toIsLeftCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :

RightCancelSemigroup (Colex α)

Equations

Colex.instRightCancelSemigroup = { toSemigroup := Colex.instSemigroup, toIsRightCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :

AddRightCancelSemigroup (Colex α)

Equations

Colex.instAddRightCancelSemigroup = { toAddSemigroup := Colex.instAddSemigroup, toIsRightCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instMulOneClass {α : Type u_1} [MulOneClass α] :

MulOneClass (Colex α)

Equations

Colex.instMulOneClass = { toOne := Colex.instOne, toMul := Colex.instMul, one_mul := ⋯, mul_one := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddZeroClass {α : Type u_1} [AddZeroClass α] :

AddZeroClass (Colex α)

Equations

Colex.instAddZeroClass = { toZero := Colex.instZero, toAdd := Colex.instAdd, zero_add := ⋯, add_zero := ⋯ }

source

@[implicit_reducible]

instance Colex.instMonoid {α : Type u_1} [Monoid α] :

Monoid (Colex α)

Equations

Colex.instMonoid = { toSemigroup := Colex.instSemigroup, toOne := Colex.instOne, one_mul := ⋯, mul_one := ⋯, npow := Colex.instMonoid._aux_3, npow_zero := ⋯, npow_succ := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddMonoid {α : Type u_1} [AddMonoid α] :

AddMonoid (Colex α)

Equations

Colex.instAddMonoid = { toAddSemigroup := Colex.instAddSemigroup, toZero := Colex.instZero, zero_add := ⋯, add_zero := ⋯, nsmul := Colex.instAddMonoid._aux_3, nsmul_zero := ⋯, nsmul_succ := ⋯ }

source

@[implicit_reducible]

instance Colex.instCommMonoid {α : Type u_1} [CommMonoid α] :

CommMonoid (Colex α)

Equations

Colex.instCommMonoid = { toMonoid := Colex.instMonoid, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :

AddCommMonoid (Colex α)

Equations

Colex.instAddCommMonoid = { toAddMonoid := Colex.instAddMonoid, add_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instLeftCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :

LeftCancelMonoid (Colex α)

Equations

Colex.instLeftCancelMonoid = { toMonoid := Colex.instMonoid, toIsLeftCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddLeftCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :

AddLeftCancelMonoid (Colex α)

Equations

Colex.instAddLeftCancelMonoid = { toAddMonoid := Colex.instAddMonoid, toIsLeftCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instRightCancelMonoid {α : Type u_1} [RightCancelMonoid α] :

RightCancelMonoid (Colex α)

Equations

Colex.instRightCancelMonoid = { toMonoid := Colex.instMonoid, toIsRightCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddRightCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :

AddRightCancelMonoid (Colex α)

Equations

Colex.instAddRightCancelMonoid = { toAddMonoid := Colex.instAddMonoid, toIsRightCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instCancelMonoid {α : Type u_1} [CancelMonoid α] :

CancelMonoid (Colex α)

Equations

Colex.instCancelMonoid = { toLeftCancelMonoid := Colex.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :

AddCancelMonoid (Colex α)

Equations

Colex.instAddCancelMonoid = { toAddLeftCancelMonoid := Colex.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :

CancelCommMonoid (Colex α)

Equations

Colex.instCancelCommMonoid = { toCommMonoid := Colex.instCommMonoid, toIsLeftCancelMul := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :

AddCancelCommMonoid (Colex α)

Equations

Colex.instAddCancelCommMonoid = { toAddCommMonoid := Colex.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }

source

@[implicit_reducible]

instance Colex.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :

InvolutiveInv (Colex α)

Equations

Colex.instInvolutiveInv = { toInv := Colex.instInv, inv_inv := ⋯ }

source

@[implicit_reducible]

instance Colex.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :

InvolutiveNeg (Colex α)

Equations

Colex.instInvolutiveNeg = { toNeg := Colex.instNeg, neg_neg := ⋯ }

source

@[implicit_reducible]

instance Colex.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :

DivInvMonoid (Colex α)

Equations

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

source

@[implicit_reducible]

instance Colex.instSubNegAddMonoid {α : Type u_1} [SubNegMonoid α] :

SubNegMonoid (Colex α)

Equations

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

source

@[implicit_reducible]

instance Colex.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :

DivisionMonoid (Colex α)

Equations

Colex.instDivisionMonoid = { toDivInvMonoid := Colex.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

source

@[implicit_reducible]

instance Colex.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :

SubtractionMonoid (Colex α)

Equations

Colex.instSubtractionMonoid = { toSubNegMonoid := Colex.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

source

@[implicit_reducible]

instance Colex.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :

DivisionCommMonoid (Colex α)

Equations

Colex.instDivisionCommMonoid = { toDivisionMonoid := Colex.instDivisionMonoid, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instDivisionAddCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :

SubtractionCommMonoid (Colex α)

Equations

Colex.instDivisionAddCommMonoid = { toSubtractionMonoid := Colex.instSubtractionMonoid, add_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instGroup {α : Type u_1} [Group α] :

Group (Colex α)

Equations

Colex.instGroup = { toDivInvMonoid := Colex.instDivInvMonoid, inv_mul_cancel := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddGroup {α : Type u_1} [AddGroup α] :

AddGroup (Colex α)

Equations

Colex.instAddGroup = { toSubNegMonoid := Colex.instSubNegAddMonoid, neg_add_cancel := ⋯ }

source

@[implicit_reducible]

instance Colex.instCommGroup {α : Type u_1} [CommGroup α] :

CommGroup (Colex α)

Equations

Colex.instCommGroup = { toGroup := Colex.instGroup, mul_comm := ⋯ }

source

@[implicit_reducible]

instance Colex.instAddCommGroup {α : Type u_1} [AddCommGroup α] :

AddCommGroup (Colex α)

Equations

Colex.instAddCommGroup = { toAddGroup := Colex.instAddGroup, add_comm := ⋯ }

source

@[simp]

theorem toColex_one {α : Type u_1} [One α] :

toColex 1 = 1

source

@[simp]

theorem toColex_zero {α : Type u_1} [Zero α] :

toColex 0 = 0

source

@[simp]

theorem toColex_eq_one {α : Type u_1} [One α] {a : α} :

toColex a = 1 ↔ a = 1

source

@[simp]

theorem toColex_eq_zero {α : Type u_1} [Zero α] {a : α} :

toColex a = 0 ↔ a = 0

source

@[simp]

theorem ofColex_one {α : Type u_1} [One α] :

ofColex 1 = 1

source

@[simp]

theorem ofColex_zero {α : Type u_1} [Zero α] :

ofColex 0 = 0

source

@[simp]

theorem ofColex_eq_one {α : Type u_1} [One α] {a : Colex α} :

ofColex a = 1 ↔ a = 1

source

@[simp]

theorem ofColex_eq_zero {α : Type u_1} [Zero α] {a : Colex α} :

ofColex a = 0 ↔ a = 0

source

@[simp]

theorem toColex_mul {α : Type u_1} [Mul α] (a b : α) :

toColex (a * b) = toColex a * toColex b

source

@[simp]

theorem toColex_add {α : Type u_1} [Add α] (a b : α) :

toColex (a + b) = toColex a + toColex b

source

@[simp]

theorem ofColex_mul {α : Type u_1} [Mul α] (a b : Colex α) :

ofColex (a * b) = ofColex a * ofColex b

source

@[simp]

theorem ofColex_add {α : Type u_1} [Add α] (a b : Colex α) :

ofColex (a + b) = ofColex a + ofColex b

source

@[simp]

theorem toColex_inv {α : Type u_1} [Inv α] (a : α) :

toColex a⁻¹ = (toColex a)⁻¹

source

@[simp]

theorem toColex_neg {α : Type u_1} [Neg α] (a : α) :

toColex (-a) = -toColex a

source

@[simp]

theorem ofColex_inv {α : Type u_1} [Inv α] (a : Colex α) :

ofColex a⁻¹ = (ofColex a)⁻¹

source

@[simp]

theorem ofColex_neg {α : Type u_1} [Neg α] (a : Colex α) :

ofColex (-a) = -ofColex a

source

@[simp]

theorem toColex_div {α : Type u_1} [Div α] (a b : α) :

toColex (a / b) = toColex a / toColex b

source

@[simp]

theorem toColex_sub {α : Type u_1} [Sub α] (a b : α) :

toColex (a - b) = toColex a - toColex b

source

@[simp]

theorem ofColex_div {α : Type u_1} [Div α] (a b : Colex α) :

ofColex (a / b) = ofColex a / ofColex b

source

@[simp]

theorem ofColex_sub {α : Type u_1} [Sub α] (a b : Colex α) :

ofColex (a - b) = ofColex a - ofColex b

source

@[simp]

theorem toColex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

toColex (a ^ b) = toColex a ^ b

source

@[simp]

theorem toColex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toColex (b • a) = b • toColex a

source

@[simp]

theorem toColex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toColex (b +ᵥ a) = b +ᵥ toColex a

source

@[simp]

theorem ofColex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : Colex α) (b : β) :

ofColex (a ^ b) = ofColex a ^ b

source

@[simp]

theorem ofColex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Colex α) :

ofColex (b +ᵥ a) = b +ᵥ ofColex a

source

@[simp]

theorem ofColex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : Colex α) :

ofColex (b • a) = b • ofColex a

source

@[simp]

theorem pow_toColex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

a ^ toColex b = a ^ b

source

@[simp]

theorem toColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toColex b +ᵥ a = b +ᵥ a

source

@[simp]

theorem toColex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toColex b • a = b • a

source

@[simp]

theorem pow_ofColex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : Colex β) :

a ^ ofColex b = a ^ b

source

@[simp]

theorem ofColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : Colex β) (a : α) :

ofColex b +ᵥ a = b +ᵥ a

source

@[simp]

theorem ofColex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Colex β) (a : α) :

ofColex b • a = b • a

source

@[simp]

theorem isLeftRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsLeftRegular (toColex a) ↔ IsLeftRegular a

source

@[simp]

theorem isAddLeftRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddLeftRegular (toColex a) ↔ IsAddLeftRegular a

source

@[simp]

theorem isLeftRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsLeftRegular (ofColex a) ↔ IsLeftRegular a

source

@[simp]

theorem isAddLeftRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} :

IsAddLeftRegular (ofColex a) ↔ IsAddLeftRegular a

source

@[simp]

theorem isRightRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsRightRegular (toColex a) ↔ IsRightRegular a

source

@[simp]

theorem isAddRightRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRightRegular (toColex a) ↔ IsAddRightRegular a

source

@[simp]

theorem isRightRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsRightRegular (ofColex a) ↔ IsRightRegular a

source

@[simp]

theorem isAddRightRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} :

IsAddRightRegular (ofColex a) ↔ IsAddRightRegular a

source

@[simp]

theorem isRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsRegular (toColex a) ↔ IsRegular a

source

@[simp]

theorem isAddRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRegular (toColex a) ↔ IsAddRegular a

source

@[simp]

theorem isRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsRegular (ofColex a) ↔ IsRegular a

source

@[simp]

theorem isAddRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} :

IsAddRegular (ofColex a) ↔ IsAddRegular a

Documentation

Mathlib.Algebra.Order.Group.Synonym

Group structure on the order type synonyms #

`OrderDual` #

Lexicographical order #

Colexicographical order #

Group structure on the order type synonyms #

OrderDual #

Lexicographical order #

Colexicographical order #

`OrderDual` #