Group structure on the order type synonyms

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

OrderDual

instance instZeroOrderDual {α : Type u_1} [h : Zero α] : Zero αᵒᵈ

instance instOneOrderDual {α : Type u_1} [h : One α] : One αᵒᵈ

instance instAddOrderDual {α : Type u_1} [h : Add α] : Add αᵒᵈ

instance instMulOrderDual {α : Type u_1} [h : Mul α] : Mul αᵒᵈ

instance instNegOrderDual {α : Type u_1} [h : Neg α] : Neg αᵒᵈ

instance instInvOrderDual {α : Type u_1} [h : Inv α] : Inv αᵒᵈ

instance instSubOrderDual {α : Type u_1} [h : Sub α] : Sub αᵒᵈ

instance instDivOrderDual {α : Type u_1} [h : Div α] : Div αᵒᵈ

instance OrderDual.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] : SMul β αᵒᵈ

instance OrderDual.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] : VAdd β αᵒᵈ

instance OrderDual.instPow {α : Type u_1} {β : Type u_2} [h : Pow α β] : Pow αᵒᵈ β

instance OrderDual.instSMul' {β : Type u_2} {α : Type u_1} [h : SMul β α] : SMul βᵒᵈ α

instance OrderDual.instVAdd' {β : Type u_2} {α : Type u_1} [h : VAdd β α] : VAdd βᵒᵈ α

instance OrderDual.instPow' {α : Type u_1} {β : Type u_2} [h : Pow α β] : Pow α βᵒᵈ

instance instAddSemigroupOrderDual {α : Type u_1} [h : AddSemigroup α] : AddSemigroup αᵒᵈ

instance instSemigroupOrderDual {α : Type u_1} [h : Semigroup α] : Semigroup αᵒᵈ

instance instAddCommSemigroupOrderDual {α : Type u_1} [h : AddCommSemigroup α] : AddCommSemigroup αᵒᵈ

instance instCommSemigroupOrderDual {α : Type u_1} [h : CommSemigroup α] : CommSemigroup αᵒᵈ

instance instAddLeftCancelSemigroupOrderDual {α : Type u_1} [h : AddLeftCancelSemigroup α] : AddLeftCancelSemigroup αᵒᵈ

instance instLeftCancelSemigroupOrderDual {α : Type u_1} [h : LeftCancelSemigroup α] : LeftCancelSemigroup αᵒᵈ

instance instAddRightCancelSemigroupOrderDual {α : Type u_1} [h : AddRightCancelSemigroup α] : AddRightCancelSemigroup αᵒᵈ

instance instRightCancelSemigroupOrderDual {α : Type u_1} [h : RightCancelSemigroup α] : RightCancelSemigroup αᵒᵈ

instance instAddZeroClassOrderDual {α : Type u_1} [h : AddZeroClass α] : AddZeroClass αᵒᵈ

instance instMulOneClassOrderDual {α : Type u_1} [h : MulOneClass α] : MulOneClass αᵒᵈ

instance instAddMonoidOrderDual {α : Type u_1} [h : AddMonoid α] : AddMonoid αᵒᵈ

instance instMonoidOrderDual {α : Type u_1} [h : Monoid α] : Monoid αᵒᵈ

instance OrderDual.instAddCommMonoid {α : Type u_1} [h : AddCommMonoid α] : AddCommMonoid αᵒᵈ

instance OrderDual.instCommMonoid {α : Type u_1} [h : CommMonoid α] : CommMonoid αᵒᵈ

instance instAddLeftCancelMonoidOrderDual {α : Type u_1} [h : AddLeftCancelMonoid α] : AddLeftCancelMonoid αᵒᵈ

instance instLeftCancelMonoidOrderDual {α : Type u_1} [h : LeftCancelMonoid α] : LeftCancelMonoid αᵒᵈ

instance instAddRightCancelMonoidOrderDual {α : Type u_1} [h : AddRightCancelMonoid α] : AddRightCancelMonoid αᵒᵈ

instance instRightCancelMonoidOrderDual {α : Type u_1} [h : RightCancelMonoid α] : RightCancelMonoid αᵒᵈ

instance instAddCancelMonoidOrderDual {α : Type u_1} [h : AddCancelMonoid α] : AddCancelMonoid αᵒᵈ

instance instCancelMonoidOrderDual {α : Type u_1} [h : CancelMonoid α] : CancelMonoid αᵒᵈ

instance OrderDual.instAddCancelCommMonoid {α : Type u_1} [h : AddCancelCommMonoid α] : AddCancelCommMonoid αᵒᵈ

instance OrderDual.instCancelCommMonoid {α : Type u_1} [h : CancelCommMonoid α] : CancelCommMonoid αᵒᵈ

instance instInvolutiveNegOrderDual {α : Type u_1} [h : InvolutiveNeg α] : InvolutiveNeg αᵒᵈ

instance instInvolutiveInvOrderDual {α : Type u_1} [h : InvolutiveInv α] : InvolutiveInv αᵒᵈ

instance instSubNegAddMonoidOrderDual {α : Type u_1} [h : SubNegMonoid α] : SubNegMonoid αᵒᵈ

instance instDivInvMonoidOrderDual {α : Type u_1} [h : DivInvMonoid α] : DivInvMonoid αᵒᵈ

instance OrderDual.subtractionMonoid {α : Type u_1} [h : SubtractionMonoid α] : SubtractionMonoid αᵒᵈ

instance instDivisionMonoidOrderDual {α : Type u_1} [h : DivisionMonoid α] : DivisionMonoid αᵒᵈ

instance OrderDual.subtractionCommMonoid {α : Type u_1} [h : SubtractionCommMonoid α] : SubtractionCommMonoid αᵒᵈ

instance instDivisionCommMonoidOrderDual {α : Type u_1} [h : DivisionCommMonoid α] : DivisionCommMonoid αᵒᵈ

instance OrderDual.instAddGroup {α : Type u_1} [h : AddGroup α] : AddGroup αᵒᵈ

instance OrderDual.instGroup {α : Type u_1} [h : Group α] : Group αᵒᵈ

instance instAddCommGroupOrderDual {α : Type u_1} [h : AddCommGroup α] : AddCommGroup αᵒᵈ

instance instCommGroupOrderDual {α : Type u_1} [h : CommGroup α] : CommGroup αᵒᵈ

@[simp]

theorem toDual_zero {α : Type u_1} [Zero α] : ↑OrderDual.toDual 0 = 0

@[simp]

theorem toDual_one {α : Type u_1} [One α] : ↑OrderDual.toDual 1 = 1

@[simp]

theorem ofDual_zero {α : Type u_1} [Zero α] : ↑OrderDual.ofDual 0 = 0

@[simp]

theorem ofDual_one {α : Type u_1} [One α] : ↑OrderDual.ofDual 1 = 1

@[simp]

theorem toDual_add {α : Type u_1} [Add α] (a : α) (b : α) : ↑OrderDual.toDual (a + b) = ↑OrderDual.toDual a + ↑OrderDual.toDual b

@[simp]

theorem toDual_mul {α : Type u_1} [Mul α] (a : α) (b : α) : ↑OrderDual.toDual (a * b) = ↑OrderDual.toDual a * ↑OrderDual.toDual b

@[simp]

theorem ofDual_add {α : Type u_1} [Add α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a + b) = ↑OrderDual.ofDual a + ↑OrderDual.ofDual b

@[simp]

theorem ofDual_mul {α : Type u_1} [Mul α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a * b) = ↑OrderDual.ofDual a * ↑OrderDual.ofDual b

@[simp]

theorem toDual_neg {α : Type u_1} [Neg α] (a : α) : ↑OrderDual.toDual (-a) = -↑OrderDual.toDual a

@[simp]

theorem toDual_inv {α : Type u_1} [Inv α] (a : α) : ↑OrderDual.toDual a⁻¹ = (↑OrderDual.toDual a)⁻¹

@[simp]

theorem ofDual_neg {α : Type u_1} [Neg α] (a : αᵒᵈ) : ↑OrderDual.ofDual (-a) = -↑OrderDual.ofDual a

@[simp]

theorem ofDual_inv {α : Type u_1} [Inv α] (a : αᵒᵈ) : ↑OrderDual.ofDual a⁻¹ = (↑OrderDual.ofDual a)⁻¹

@[simp]

theorem toDual_sub {α : Type u_1} [Sub α] (a : α) (b : α) : ↑OrderDual.toDual (a - b) = ↑OrderDual.toDual a - ↑OrderDual.toDual b

@[simp]

theorem toDual_div {α : Type u_1} [Div α] (a : α) (b : α) : ↑OrderDual.toDual (a / b) = ↑OrderDual.toDual a / ↑OrderDual.toDual b

@[simp]

theorem ofDual_sub {α : Type u_1} [Sub α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a - b) = ↑OrderDual.ofDual a - ↑OrderDual.ofDual b

@[simp]

theorem ofDual_div {α : Type u_1} [Div α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a / b) = ↑OrderDual.ofDual a / ↑OrderDual.ofDual b

@[simp]

theorem toDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : ↑OrderDual.toDual (b • a) = b • ↑OrderDual.toDual a

@[simp]

theorem toDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : ↑OrderDual.toDual (b +ᵥ a) = b +ᵥ ↑OrderDual.toDual a

@[simp]

theorem toDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) : ↑OrderDual.toDual (a ^ b) = ↑OrderDual.toDual a ^ b

@[simp]

theorem ofDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : αᵒᵈ) : ↑OrderDual.ofDual (b • a) = b • ↑OrderDual.ofDual a

@[simp]

theorem ofDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : αᵒᵈ) : ↑OrderDual.ofDual (b +ᵥ a) = b +ᵥ ↑OrderDual.ofDual a

@[simp]

theorem ofDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵒᵈ) (b : β) : ↑OrderDual.ofDual (a ^ b) = ↑OrderDual.ofDual a ^ b

@[simp]

theorem toDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : ↑OrderDual.toDual b • a = b • a

@[simp]

theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : ↑OrderDual.toDual b +ᵥ a = b +ᵥ a

@[simp]

theorem pow_toDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) : a ^ ↑OrderDual.toDual b = a ^ b

@[simp]

theorem ofDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : βᵒᵈ) (a : α) : ↑OrderDual.ofDual b +ᵥ a = b +ᵥ a

@[simp]

theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : βᵒᵈ) (a : α) : ↑OrderDual.ofDual b • a = b • a

@[simp]

theorem pow_ofDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ↑OrderDual.ofDual b = a ^ b

Lexicographical order

instance instZeroLex {α : Type u_1} [h : Zero α] : Zero (Lex α)

instance instOneLex {α : Type u_1} [h : One α] : One (Lex α)

instance instAddLex {α : Type u_1} [h : Add α] : Add (Lex α)

instance instMulLex {α : Type u_1} [h : Mul α] : Mul (Lex α)

instance instNegLex {α : Type u_1} [h : Neg α] : Neg (Lex α)

instance instInvLex {α : Type u_1} [h : Inv α] : Inv (Lex α)

instance instSubLex {α : Type u_1} [h : Sub α] : Sub (Lex α)

instance instDivLex {α : Type u_1} [h : Div α] : Div (Lex α)

instance Lex.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] : VAdd β (Lex α)

instance Lex.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] : SMul β (Lex α)

instance Lex.instPow {α : Type u_1} {β : Type u_2} [h : Pow α β] : Pow (Lex α) β

instance Lex.instSMul' {β : Type u_2} {α : Type u_1} [h : SMul β α] : SMul (Lex β) α

instance Lex.instVAdd' {β : Type u_2} {α : Type u_1} [h : VAdd β α] : VAdd (Lex β) α

instance Lex.instPow' {α : Type u_1} {β : Type u_2} [h : Pow α β] : Pow α (Lex β)

instance instAddSemigroupLex {α : Type u_1} [h : AddSemigroup α] : AddSemigroup (Lex α)

instance instSemigroupLex {α : Type u_1} [h : Semigroup α] : Semigroup (Lex α)

instance instAddCommSemigroupLex {α : Type u_1} [h : AddCommSemigroup α] : AddCommSemigroup (Lex α)

instance instCommSemigroupLex {α : Type u_1} [h : CommSemigroup α] : CommSemigroup (Lex α)

instance instAddLeftCancelSemigroupLex {α : Type u_1} [h : AddLeftCancelSemigroup α] : AddLeftCancelSemigroup (Lex α)

instance instLeftCancelSemigroupLex {α : Type u_1} [h : LeftCancelSemigroup α] : LeftCancelSemigroup (Lex α)

instance instAddRightCancelSemigroupLex {α : Type u_1} [h : AddRightCancelSemigroup α] : AddRightCancelSemigroup (Lex α)

instance instRightCancelSemigroupLex {α : Type u_1} [h : RightCancelSemigroup α] : RightCancelSemigroup (Lex α)

instance instAddZeroClassLex {α : Type u_1} [h : AddZeroClass α] : AddZeroClass (Lex α)

instance instMulOneClassLex {α : Type u_1} [h : MulOneClass α] : MulOneClass (Lex α)

instance instAddMonoidLex {α : Type u_1} [h : AddMonoid α] : AddMonoid (Lex α)

instance instMonoidLex {α : Type u_1} [h : Monoid α] : Monoid (Lex α)

instance instAddCommMonoidLex {α : Type u_1} [h : AddCommMonoid α] : AddCommMonoid (Lex α)

instance instCommMonoidLex {α : Type u_1} [h : CommMonoid α] : CommMonoid (Lex α)

instance instAddLeftCancelMonoidLex {α : Type u_1} [h : AddLeftCancelMonoid α] : AddLeftCancelMonoid (Lex α)

instance instLeftCancelMonoidLex {α : Type u_1} [h : LeftCancelMonoid α] : LeftCancelMonoid (Lex α)

instance instAddRightCancelMonoidLex {α : Type u_1} [h : AddRightCancelMonoid α] : AddRightCancelMonoid (Lex α)

instance instRightCancelMonoidLex {α : Type u_1} [h : RightCancelMonoid α] : RightCancelMonoid (Lex α)

instance instAddCancelMonoidLex {α : Type u_1} [h : AddCancelMonoid α] : AddCancelMonoid (Lex α)

instance instCancelMonoidLex {α : Type u_1} [h : CancelMonoid α] : CancelMonoid (Lex α)

instance instAddCancelCommMonoidLex {α : Type u_1} [h : AddCancelCommMonoid α] : AddCancelCommMonoid (Lex α)

instance instCancelCommMonoidLex {α : Type u_1} [h : CancelCommMonoid α] : CancelCommMonoid (Lex α)

instance instInvolutiveNegLex {α : Type u_1} [h : InvolutiveNeg α] : InvolutiveNeg (Lex α)

instance instInvolutiveInvLex {α : Type u_1} [h : InvolutiveInv α] : InvolutiveInv (Lex α)

instance instSubNegAddMonoidLex {α : Type u_1} [h : SubNegMonoid α] : SubNegMonoid (Lex α)

instance instDivInvMonoidLex {α : Type u_1} [h : DivInvMonoid α] : DivInvMonoid (Lex α)

instance instDivisionMonoidLex {α : Type u_1} [h : DivisionMonoid α] : DivisionMonoid (Lex α)

instance instDivisionCommMonoidLex {α : Type u_1} [h : DivisionCommMonoid α] : DivisionCommMonoid (Lex α)

instance instAddGroupLex {α : Type u_1} [h : AddGroup α] : AddGroup (Lex α)

instance instGroupLex {α : Type u_1} [h : Group α] : Group (Lex α)

instance instAddCommGroupLex {α : Type u_1} [h : AddCommGroup α] : AddCommGroup (Lex α)

instance instCommGroupLex {α : Type u_1} [h : CommGroup α] : CommGroup (Lex α)

@[simp]

theorem toLex_zero {α : Type u_1} [Zero α] : ↑toLex 0 = 0

@[simp]

theorem toLex_one {α : Type u_1} [One α] : ↑toLex 1 = 1

@[simp]

theorem ofLex_zero {α : Type u_1} [Zero α] : ↑ofLex 0 = 0

@[simp]

theorem ofLex_one {α : Type u_1} [One α] : ↑ofLex 1 = 1

@[simp]

theorem toLex_add {α : Type u_1} [Add α] (a : α) (b : α) : ↑toLex (a + b) = ↑toLex a + ↑toLex b

@[simp]

theorem toLex_mul {α : Type u_1} [Mul α] (a : α) (b : α) : ↑toLex (a * b) = ↑toLex a * ↑toLex b

@[simp]

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

@[simp]

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

@[simp]

theorem toLex_neg {α : Type u_1} [Neg α] (a : α) : ↑toLex (-a) = -↑toLex a

@[simp]

theorem toLex_inv {α : Type u_1} [Inv α] (a : α) : ↑toLex a⁻¹ = (↑toLex a)⁻¹

@[simp]

theorem ofLex_neg {α : Type u_1} [Neg α] (a : Lex α) : ↑ofLex (-a) = -↑ofLex a

@[simp]

theorem ofLex_inv {α : Type u_1} [Inv α] (a : Lex α) : ↑ofLex a⁻¹ = (↑ofLex a)⁻¹

@[simp]

theorem toLex_sub {α : Type u_1} [Sub α] (a : α) (b : α) : ↑toLex (a - b) = ↑toLex a - ↑toLex b

@[simp]

theorem toLex_div {α : Type u_1} [Div α] (a : α) (b : α) : ↑toLex (a / b) = ↑toLex a / ↑toLex b

@[simp]

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

@[simp]

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

@[simp]

theorem toLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : ↑toLex (b +ᵥ a) = b +ᵥ ↑toLex a

@[simp]

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

@[simp]

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

@[simp]

theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Lex α) : ↑ofLex (b +ᵥ a) = b +ᵥ ↑ofLex a

@[simp]

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

@[simp]

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

@[simp]

theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : ↑toLex b +ᵥ a = b +ᵥ a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : Lex β) (a : α) : ↑ofLex b +ᵥ a = b +ᵥ a

@[simp]

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