# Documentation

Mathlib.Algebra.Group.OrderSynonym

# Group structure on the order type synonyms #

Transfer algebraic instances from α to αᵒᵈ and lex α.

### OrderDual#

instance instZeroOrderDual {α : Type u_1} [h : Zero α] :
Equations
• instZeroOrderDual = h
instance instOneOrderDual {α : Type u_1} [h : One α] :
Equations
• instOneOrderDual = h
Equations
instance instMulOrderDual {α : Type u_1} [h : Mul α] :
Equations
• instMulOrderDual = h
instance instNegOrderDual {α : Type u_1} [h : Neg α] :
Equations
• instNegOrderDual = h
instance instInvOrderDual {α : Type u_1} [h : Inv α] :
Equations
• instInvOrderDual = h
instance instSubOrderDual {α : Type u_1} [h : Sub α] :
Equations
• instSubOrderDual = h
instance instDivOrderDual {α : Type u_1} [h : Div α] :
Equations
• instDivOrderDual = h
instance instVAddOrderDual {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
Equations
instance instSMulOrderDual {β : Type u_2} {α : Type u_1} [h : SMul β α] :
Equations
• instSMulOrderDual = h
instance instPowOrderDual {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow αᵒᵈ β
Equations
• instPowOrderDual = h
instance instSMulOrderDual' {β : Type u_2} {α : Type u_1} [h : SMul β α] :
Equations
• instSMulOrderDual' = h
instance instVAddOrderDual' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
Equations
instance instPowOrderDual' {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow α βᵒᵈ
Equations
• instPowOrderDual' = h
instance instAddSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
• instSemigroupOrderDual = h
instance instAddCommSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instCommSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
• instCommSemigroupOrderDual = h
instance instAddLeftCancelSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instLeftCancelSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
• instLeftCancelSemigroupOrderDual = h
instance instAddRightCancelSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instRightCancelSemigroupOrderDual {α : Type u_1} [h : ] :
Equations
• instRightCancelSemigroupOrderDual = h
instance instAddZeroClassOrderDual {α : Type u_1} [h : ] :
Equations
instance instMulOneClassOrderDual {α : Type u_1} [h : ] :
Equations
• instMulOneClassOrderDual = h
instance instAddMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instMonoidOrderDual = h
instance instAddCommMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instCommMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instCommMonoidOrderDual = h
instance instAddLeftCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instLeftCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instLeftCancelMonoidOrderDual = h
instance instAddRightCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instRightCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instRightCancelMonoidOrderDual = h
instance instAddCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instCancelMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instCancelMonoidOrderDual = h
instance instAddCancelCommMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instCancelCommMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instCancelCommMonoidOrderDual = h
instance instInvolutiveNegOrderDual {α : Type u_1} [h : ] :
Equations
• instInvolutiveNegOrderDual = h
instance instInvolutiveInvOrderDual {α : Type u_1} [h : ] :
Equations
• instInvolutiveInvOrderDual = h
instance instSubNegAddMonoidOrderDual {α : Type u_1} [h : ] :
Equations
instance instDivInvMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instDivInvMonoidOrderDual = h
instance OrderDual.subtractionMonoid {α : Type u_1} [h : ] :
Equations
• OrderDual.subtractionMonoid = h
instance instDivisionMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instDivisionMonoidOrderDual = h
instance OrderDual.subtractionCommMonoid {α : Type u_1} [h : ] :
Equations
• OrderDual.subtractionCommMonoid = h
instance instDivisionCommMonoidOrderDual {α : Type u_1} [h : ] :
Equations
• instDivisionCommMonoidOrderDual = h
instance instAddGroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instGroupOrderDual {α : Type u_1} [h : ] :
Equations
• instGroupOrderDual = h
instance instAddCommGroupOrderDual {α : Type u_1} [h : ] :
Equations
instance instCommGroupOrderDual {α : Type u_1} [h : ] :
Equations
• instCommGroupOrderDual = h
@[simp]
theorem toDual_zero {α : Type u_1} [inst : Zero α] :
OrderDual.toDual 0 = 0
@[simp]
theorem toDual_one {α : Type u_1} [inst : One α] :
OrderDual.toDual 1 = 1
@[simp]
theorem ofDual_zero {α : Type u_1} [inst : Zero α] :
OrderDual.ofDual 0 = 0
@[simp]
theorem ofDual_one {α : Type u_1} [inst : One α] :
OrderDual.ofDual 1 = 1
@[simp]
theorem toDual_add {α : Type u_1} [inst : Add α] (a : α) (b : α) :
OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b
@[simp]
theorem toDual_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b
@[simp]
theorem ofDual_add {α : Type u_1} [inst : Add α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a + b) = OrderDual.ofDual a + OrderDual.ofDual b
@[simp]
theorem ofDual_mul {α : Type u_1} [inst : Mul α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a * b) = OrderDual.ofDual a * OrderDual.ofDual b
@[simp]
theorem toDual_neg {α : Type u_1} [inst : Neg α] (a : α) :
OrderDual.toDual (-a) = -OrderDual.toDual a
@[simp]
theorem toDual_inv {α : Type u_1} [inst : Inv α] (a : α) :
OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹
@[simp]
theorem ofDual_neg {α : Type u_1} [inst : Neg α] (a : αᵒᵈ) :
OrderDual.ofDual (-a) = -OrderDual.ofDual a
@[simp]
theorem ofDual_inv {α : Type u_1} [inst : Inv α] (a : αᵒᵈ) :
OrderDual.ofDual a⁻¹ = (OrderDual.ofDual a)⁻¹
@[simp]
theorem toDual_sub {α : Type u_1} [inst : Sub α] (a : α) (b : α) :
OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b
@[simp]
theorem toDual_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b
@[simp]
theorem ofDual_sub {α : Type u_1} [inst : Sub α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a - b) = OrderDual.ofDual a - OrderDual.ofDual b
@[simp]
theorem ofDual_div {α : Type u_1} [inst : Div α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a / b) = OrderDual.ofDual a / OrderDual.ofDual b
@[simp]
theorem toDual_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
@[simp]
theorem toDual_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
OrderDual.toDual (b a) = b OrderDual.toDual a
@[simp]
theorem toDual_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b
@[simp]
theorem ofDual_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : αᵒᵈ) :
OrderDual.ofDual (b +ᵥ a) = b +ᵥ OrderDual.ofDual a
@[simp]
theorem ofDual_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : αᵒᵈ) :
OrderDual.ofDual (b a) = b OrderDual.ofDual a
@[simp]
theorem ofDual_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : αᵒᵈ) (b : β) :
OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b
@[simp]
theorem toDual_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
OrderDual.toDual b a = b a
@[simp]
theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
OrderDual.toDual b +ᵥ a = b +ᵥ a
@[simp]
theorem pow_toDual {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
a ^ OrderDual.toDual b = a ^ b
@[simp]
theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : βᵒᵈ) (a : α) :
OrderDual.ofDual b a = b a
@[simp]
theorem ofDual_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : βᵒᵈ) (a : α) :
OrderDual.ofDual b +ᵥ a = b +ᵥ a
@[simp]
theorem pow_ofDual {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : βᵒᵈ) :
a ^ OrderDual.ofDual b = a ^ b

### Lexicographical order #

instance instZeroLex {α : Type u_1} [h : Zero α] :
Zero (Lex α)
Equations
• instZeroLex = h
instance instOneLex {α : Type u_1} [h : One α] :
One (Lex α)
Equations
• instOneLex = h
Equations
instance instMulLex {α : Type u_1} [h : Mul α] :
Mul (Lex α)
Equations
• instMulLex = h
instance instNegLex {α : Type u_1} [h : Neg α] :
Neg (Lex α)
Equations
• instNegLex = h
instance instInvLex {α : Type u_1} [h : Inv α] :
Inv (Lex α)
Equations
• instInvLex = h
instance instSubLex {α : Type u_1} [h : Sub α] :
Sub (Lex α)
Equations
• instSubLex = h
instance instDivLex {α : Type u_1} [h : Div α] :
Div (Lex α)
Equations
• instDivLex = h
instance instSMulLex {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul β (Lex α)
Equations
• instSMulLex = h
instance instVAddLex {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
Equations
instance instPowLex {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow (Lex α) β
Equations
• instPowLex = h
instance instSMulLex' {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul (Lex β) α
Equations
• instSMulLex' = h
instance instVAddLex' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
Equations
instance instPowLex' {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow α (Lex β)
Equations
• instPowLex' = h
instance instAddSemigroupLex {α : Type u_1} [h : ] :
Equations
instance instSemigroupLex {α : Type u_1} [h : ] :
Equations
• instSemigroupLex = h
instance instAddCommSemigroupLex {α : Type u_1} [h : ] :
Equations
instance instCommSemigroupLex {α : Type u_1} [h : ] :
Equations
• instCommSemigroupLex = h
instance instAddLeftCancelSemigroupLex {α : Type u_1} [h : ] :
Equations
instance instLeftCancelSemigroupLex {α : Type u_1} [h : ] :
Equations
• instLeftCancelSemigroupLex = h
instance instAddRightCancelSemigroupLex {α : Type u_1} [h : ] :
Equations
instance instRightCancelSemigroupLex {α : Type u_1} [h : ] :
Equations
• instRightCancelSemigroupLex = h
instance instAddZeroClassLex {α : Type u_1} [h : ] :
Equations
instance instMulOneClassLex {α : Type u_1} [h : ] :
Equations
• instMulOneClassLex = h
instance instAddMonoidLex {α : Type u_1} [h : ] :
Equations
instance instMonoidLex {α : Type u_1} [h : ] :
Monoid (Lex α)
Equations
• instMonoidLex = h
instance instAddCommMonoidLex {α : Type u_1} [h : ] :
Equations
instance instCommMonoidLex {α : Type u_1} [h : ] :
Equations
• instCommMonoidLex = h
instance instAddLeftCancelMonoidLex {α : Type u_1} [h : ] :
Equations
instance instLeftCancelMonoidLex {α : Type u_1} [h : ] :
Equations
• instLeftCancelMonoidLex = h
instance instAddRightCancelMonoidLex {α : Type u_1} [h : ] :
Equations
instance instRightCancelMonoidLex {α : Type u_1} [h : ] :
Equations
• instRightCancelMonoidLex = h
instance instAddCancelMonoidLex {α : Type u_1} [h : ] :
Equations
instance instCancelMonoidLex {α : Type u_1} [h : ] :
Equations
• instCancelMonoidLex = h
instance instAddCancelCommMonoidLex {α : Type u_1} [h : ] :
Equations
instance instCancelCommMonoidLex {α : Type u_1} [h : ] :
Equations
• instCancelCommMonoidLex = h
instance instInvolutiveNegLex {α : Type u_1} [h : ] :
Equations
• instInvolutiveNegLex = h
instance instInvolutiveInvLex {α : Type u_1} [h : ] :
Equations
• instInvolutiveInvLex = h
instance instSubNegAddMonoidLex {α : Type u_1} [h : ] :
Equations
instance instDivInvMonoidLex {α : Type u_1} [h : ] :
Equations
• instDivInvMonoidLex = h
instance instDivisionMonoidLex {α : Type u_1} [h : ] :
Equations
• instDivisionMonoidLex = h
instance instDivisionCommMonoidLex {α : Type u_1} [h : ] :
Equations
• instDivisionCommMonoidLex = h
instance instAddGroupLex {α : Type u_1} [h : ] :
Equations
instance instGroupLex {α : Type u_1} [h : ] :
Group (Lex α)
Equations
• instGroupLex = h
instance instAddCommGroupLex {α : Type u_1} [h : ] :
Equations
instance instCommGroupLex {α : Type u_1} [h : ] :
Equations
• instCommGroupLex = h
@[simp]
theorem toLex_zero {α : Type u_1} [inst : Zero α] :
toLex 0 = 0
@[simp]
theorem toLex_one {α : Type u_1} [inst : One α] :
toLex 1 = 1
@[simp]
theorem ofLex_zero {α : Type u_1} [inst : Zero α] :
ofLex 0 = 0
@[simp]
theorem ofLex_one {α : Type u_1} [inst : One α] :
ofLex 1 = 1
@[simp]
theorem toLex_add {α : Type u_1} [inst : Add α] (a : α) (b : α) :
toLex (a + b) = toLex a + toLex b
@[simp]
theorem toLex_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
toLex (a * b) = toLex a * toLex b
@[simp]
theorem ofLex_add {α : Type u_1} [inst : Add α] (a : Lex α) (b : Lex α) :
ofLex (a + b) = ofLex a + ofLex b
@[simp]
theorem ofLex_mul {α : Type u_1} [inst : Mul α] (a : Lex α) (b : Lex α) :
ofLex (a * b) = ofLex a * ofLex b
@[simp]
theorem toLex_neg {α : Type u_1} [inst : Neg α] (a : α) :
toLex (-a) = -toLex a
@[simp]
theorem toLex_inv {α : Type u_1} [inst : Inv α] (a : α) :
toLex a⁻¹ = (toLex a)⁻¹
@[simp]
theorem ofLex_neg {α : Type u_1} [inst : Neg α] (a : Lex α) :
ofLex (-a) = -ofLex a
@[simp]
theorem ofLex_inv {α : Type u_1} [inst : Inv α] (a : Lex α) :
ofLex a⁻¹ = (ofLex a)⁻¹
@[simp]
theorem toLex_sub {α : Type u_1} [inst : Sub α] (a : α) (b : α) :
toLex (a - b) = toLex a - toLex b
@[simp]
theorem toLex_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
toLex (a / b) = toLex a / toLex b
@[simp]
theorem ofLex_sub {α : Type u_1} [inst : Sub α] (a : Lex α) (b : Lex α) :
ofLex (a - b) = ofLex a - ofLex b
@[simp]
theorem ofLex_div {α : Type u_1} [inst : Div α] (a : Lex α) (b : Lex α) :
ofLex (a / b) = ofLex a / ofLex b
@[simp]
theorem toLex_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
toLex (b a) = b toLex a
@[simp]
theorem toLex_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
toLex (b +ᵥ a) = b +ᵥ toLex a
@[simp]
theorem toLex_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
toLex (a ^ b) = toLex a ^ b
@[simp]
theorem ofLex_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : Lex α) :
ofLex (b a) = b ofLex a
@[simp]
theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : Lex α) :
ofLex (b +ᵥ a) = b +ᵥ ofLex a
@[simp]
theorem ofLex_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : Lex α) (b : β) :
ofLex (a ^ b) = ofLex a ^ b
@[simp]
theorem toLex_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
toLex b a = b a
@[simp]
theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
toLex b +ᵥ a = b +ᵥ a
@[simp]
theorem pow_toLex {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
a ^ toLex b = a ^ b
@[simp]
theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : Lex β) (a : α) :
ofLex b +ᵥ a = b +ᵥ a
@[simp]
theorem ofLex_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : Lex β) (a : α) :
ofLex b a = b a
@[simp]
theorem pow_ofLex {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : Lex β) :
a ^ ofLex b = a ^ b