Documentation

Mathlib.Algebra.Order.Group.Synonym

Group structure on the order type synonyms #

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

OrderDual #

source
@[implicit_reducible]
instance OrderDual.instOne {α : Type u_1} [One α] :
One αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instZero {α : Type u_1} [Zero α] :
Zero αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instMul {α : Type u_1} [Mul α] :
Mul αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAdd {α : Type u_1} [Add α] :
Add αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instInv {α : Type u_1} [Inv α] :
Inv αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNeg {α : Type u_1} [Neg α] :
Neg αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instDiv {α : Type u_1} [Div α] :
Div αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSub {α : Type u_1} [Sub α] :
Sub αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instPow {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow αᵒᵈ β
source
@[implicit_reducible]
instance OrderDual.instSMul {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul β αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instVAdd {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd β αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instPow_1 {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow α βᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instVAdd' {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd βᵒᵈ α
source
@[implicit_reducible]
instance OrderDual.instSMul' {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul βᵒᵈ α
source
@[implicit_reducible]
instance OrderDual.instSemigroup {α : Type u_1} [Semigroup α] :
Semigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
CommSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
AddCommSemigroup αᵒᵈ
source
instance OrderDual.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :
IsLeftCancelMul αᵒᵈ
source
instance OrderDual.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
IsLeftCancelAdd αᵒᵈ
source
instance OrderDual.instIsRightCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :
IsRightCancelMul αᵒᵈ
source
instance OrderDual.instIsRightCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :
IsRightCancelAdd αᵒᵈ
source
instance OrderDual.instIsCancelMul {α : Type u_1} [Mul α] [IsCancelMul α] :
IsCancelMul αᵒᵈ
source
instance OrderDual.instIsCancelAdd {α : Type u_1} [Add α] [IsCancelAdd α] :
IsCancelAdd αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
LeftCancelSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
RightCancelSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
AddRightCancelSemigroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instMulOneClass {α : Type u_1} [MulOneClass α] :
MulOneClass αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
AddZeroClass αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instMonoid {α : Type u_1} [Monoid α] :
Monoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddMonoid {α : Type u_1} [AddMonoid α] :
AddMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommMonoid {α : Type u_1} [CommMonoid α] :
CommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
AddCommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instLeftCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :
LeftCancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddLeftCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :
AddLeftCancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instRightCancelMonoid {α : Type u_1} [RightCancelMonoid α] :
RightCancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddRightCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :
AddRightCancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCancelMonoid {α : Type u_1} [CancelMonoid α] :
CancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :
AddCancelMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :
CancelCommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :
AddCancelCommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :
InvolutiveInv αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :
InvolutiveNeg αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
DivInvMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSubNegAddMonoid {α : Type u_1} [SubNegMonoid α] :
SubNegMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :
DivisionMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :
SubtractionMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :
DivisionCommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instDivisionAddCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :
SubtractionCommMonoid αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instGroup {α : Type u_1} [Group α] :
Group αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddGroup {α : Type u_1} [AddGroup α] :
AddGroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommGroup {α : Type u_1} [CommGroup α] :
CommGroup αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
AddCommGroup αᵒᵈ
source
@[simp]
theorem toDual_one {α : Type u_1} [One α] :
OrderDual.toDual 1 = 1
source
@[simp]
theorem toDual_zero {α : Type u_1} [Zero α] :
OrderDual.toDual 0 = 0
source
@[simp]
theorem ofDual_one {α : Type u_1} [One α] :
OrderDual.ofDual 1 = 1
source
@[simp]
theorem ofDual_zero {α : Type u_1} [Zero α] :
OrderDual.ofDual 0 = 0
source
@[simp]
theorem toDual_eq_one {α : Type u_1} [One α] {a : α} :
OrderDual.toDual a = 1 ↔ a = 1
source
@[simp]
theorem toDual_eq_zero {α : Type u_1} [Zero α] {a : α} :
OrderDual.toDual a = 0 ↔ a = 0
source
@[simp]
theorem ofDual_eq_one {α : Type u_1} [One α] {a : αᵒᵈ} :
OrderDual.ofDual a = 1 ↔ a = 1
source
@[simp]
theorem ofDual_eq_zero {α : Type u_1} [Zero α] {a : αᵒᵈ} :
OrderDual.ofDual a = 0 ↔ a = 0
source
@[simp]
theorem toDual_mul {α : Type u_1} [Mul α] (a b : α) :
OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b
source
@[simp]
theorem toDual_add {α : Type u_1} [Add α] (a b : α) :
OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b
source
@[simp]
theorem ofDual_mul {α : Type u_1} [Mul α] (a b : αᵒᵈ) :
OrderDual.ofDual (a * b) = OrderDual.ofDual a * OrderDual.ofDual b
source
@[simp]
theorem ofDual_add {α : Type u_1} [Add α] (a b : αᵒᵈ) :
OrderDual.ofDual (a + b) = OrderDual.ofDual a + OrderDual.ofDual b
source
@[simp]
theorem toDual_inv {α : Type u_1} [Inv α] (a : α) :
OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹
source
@[simp]
theorem toDual_neg {α : Type u_1} [Neg α] (a : α) :
OrderDual.toDual (-a) = -OrderDual.toDual a
source
@[simp]
theorem ofDual_inv {α : Type u_1} [Inv α] (a : αᵒᵈ) :
OrderDual.ofDual a⁻¹ = (OrderDual.ofDual a)⁻¹
source
@[simp]
theorem ofDual_neg {α : Type u_1} [Neg α] (a : αᵒᵈ) :
OrderDual.ofDual (-a) = -OrderDual.ofDual a
source
@[simp]
theorem toDual_div {α : Type u_1} [Div α] (a b : α) :
OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b
source
@[simp]
theorem toDual_sub {α : Type u_1} [Sub α] (a b : α) :
OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b
source
@[simp]
theorem ofDual_div {α : Type u_1} [Div α] (a b : αᵒᵈ) :
OrderDual.ofDual (a / b) = OrderDual.ofDual a / OrderDual.ofDual b
source
@[simp]
theorem ofDual_sub {α : Type u_1} [Sub α] (a b : αᵒᵈ) :
OrderDual.ofDual (a - b) = OrderDual.ofDual a - OrderDual.ofDual b
source
@[simp]
theorem toDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b
source
@[simp]
theorem toDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
source
@[simp]
theorem toDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
OrderDual.toDual (b • a) = b • OrderDual.toDual a
source
@[simp]
theorem ofDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵒᵈ) (b : β) :
OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b
source
@[simp]
theorem ofDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : αᵒᵈ) :
OrderDual.ofDual (b +ᵥ a) = b +ᵥ OrderDual.ofDual a
source
@[simp]
theorem ofDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : αᵒᵈ) :
OrderDual.ofDual (b • a) = b • OrderDual.ofDual a
source
@[simp]
theorem pow_toDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
a ^ OrderDual.toDual b = a ^ b
source
@[simp]
theorem toDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
OrderDual.toDual b • a = b • a
source
@[simp]
theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
OrderDual.toDual b +ᵥ a = b +ᵥ a
source
@[simp]
theorem pow_ofDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : βᵒᵈ) :
a ^ OrderDual.ofDual b = a ^ b
source
@[simp]
theorem ofDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : βᵒᵈ) (a : α) :
OrderDual.ofDual b +ᵥ a = b +ᵥ a
source
@[simp]
theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : βᵒᵈ) (a : α) :
OrderDual.ofDual b • a = b • a
source
@[simp]
theorem isLeftRegular_toDual {α : Type u_1} [Monoid α] {a : α} :
IsLeftRegular (OrderDual.toDual a) ↔ IsLeftRegular a
source
@[simp]
theorem isAddLeftRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :
IsAddLeftRegular (OrderDual.toDual a) ↔ IsAddLeftRegular a
source
@[simp]
theorem isLeftRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :
IsLeftRegular (OrderDual.ofDual a) ↔ IsLeftRegular a
source
@[simp]
theorem isAddLeftRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :
IsAddLeftRegular (OrderDual.ofDual a) ↔ IsAddLeftRegular a
source
@[simp]
theorem isRightRegular_toDual {α : Type u_1} [Monoid α] {a : α} :
IsRightRegular (OrderDual.toDual a) ↔ IsRightRegular a
source
@[simp]
theorem isAddRightRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :
IsAddRightRegular (OrderDual.toDual a) ↔ IsAddRightRegular a
source
@[simp]
theorem isRightRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :
IsRightRegular (OrderDual.ofDual a) ↔ IsRightRegular a
source
@[simp]
theorem isAddRightRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :
IsAddRightRegular (OrderDual.ofDual a) ↔ IsAddRightRegular a
source
@[simp]
theorem isRegular_toDual {α : Type u_1} [Monoid α] {a : α} :
IsRegular (OrderDual.toDual a) ↔ IsRegular a
source
@[simp]
theorem isAddRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :
IsAddRegular (OrderDual.toDual a) ↔ IsAddRegular a
source
@[simp]
theorem isRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :
IsRegular (OrderDual.ofDual a) ↔ IsRegular a
source
@[simp]
theorem isAddRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :
IsAddRegular (OrderDual.ofDual a) ↔ IsAddRegular a

Lexicographical order #

source
@[implicit_reducible]
instance Lex.instOne {α : Type u_1} [One α] :
One (Lex α)
source
@[implicit_reducible]
instance Lex.instZero {α : Type u_1} [Zero α] :
Zero (Lex α)
source
@[implicit_reducible]
instance Lex.instMul {α : Type u_1} [Mul α] :
Mul (Lex α)
source
@[implicit_reducible]
instance Lex.instAdd {α : Type u_1} [Add α] :
Add (Lex α)
source
@[implicit_reducible]
instance Lex.instInv {α : Type u_1} [Inv α] :
Inv (Lex α)
source
@[implicit_reducible]
instance Lex.instNeg {α : Type u_1} [Neg α] :
Neg (Lex α)
source
@[implicit_reducible]
instance Lex.instDiv {α : Type u_1} [Div α] :
Div (Lex α)
source
@[implicit_reducible]
instance Lex.instSub {α : Type u_1} [Sub α] :
Sub (Lex α)
source
@[implicit_reducible]
instance Lex.instPow {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow (Lex α) β
source
@[implicit_reducible]
instance Lex.instSMul {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul β (Lex α)
source
@[implicit_reducible]
instance Lex.instVAdd {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd β (Lex α)
source
@[implicit_reducible]
instance Lex.instPow_1 {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow α (Lex β)
source
@[implicit_reducible]
instance Lex.instSMul' {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul (Lex β) α
source
@[implicit_reducible]
instance Lex.instVAdd' {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd (Lex β) α
source
@[implicit_reducible]
instance Lex.instSemigroup {α : Type u_1} [Semigroup α] :
Semigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
CommSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
AddCommSemigroup (Lex α)
source
instance Lex.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :
IsLeftCancelMul (Lex α)
source
instance Lex.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
IsLeftCancelAdd (Lex α)
source
instance Lex.instIsRightCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :
IsRightCancelMul (Lex α)
source
instance Lex.instIsRightCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :
IsRightCancelAdd (Lex α)
source
instance Lex.instIsCancelMul {α : Type u_1} [Mul α] [IsCancelMul α] :
IsCancelMul (Lex α)
source
instance Lex.instIsCancelAdd {α : Type u_1} [Add α] [IsCancelAdd α] :
IsCancelAdd (Lex α)
source
@[implicit_reducible]
instance Lex.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
LeftCancelSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
RightCancelSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
AddRightCancelSemigroup (Lex α)
source
@[implicit_reducible]
instance Lex.instMulOneClass {α : Type u_1} [MulOneClass α] :
MulOneClass (Lex α)
source
@[implicit_reducible]
instance Lex.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
AddZeroClass (Lex α)
source
@[implicit_reducible]
instance Lex.instMonoid {α : Type u_1} [Monoid α] :
Monoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddMonoid {α : Type u_1} [AddMonoid α] :
AddMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instCommMonoid {α : Type u_1} [CommMonoid α] :
CommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
AddCommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instLeftCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :
LeftCancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddLeftCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :
AddLeftCancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instRightCancelMonoid {α : Type u_1} [RightCancelMonoid α] :
RightCancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddRightCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :
AddRightCancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instCancelMonoid {α : Type u_1} [CancelMonoid α] :
CancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :
AddCancelMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :
CancelCommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :
AddCancelCommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :
InvolutiveInv (Lex α)
source
@[implicit_reducible]
instance Lex.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :
InvolutiveNeg (Lex α)
source
@[implicit_reducible]
instance Lex.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
DivInvMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instSubNegAddMonoid {α : Type u_1} [SubNegMonoid α] :
SubNegMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :
DivisionMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :
SubtractionMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :
DivisionCommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instDivisionAddCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :
SubtractionCommMonoid (Lex α)
source
@[implicit_reducible]
instance Lex.instGroup {α : Type u_1} [Group α] :
Group (Lex α)
source
@[implicit_reducible]
instance Lex.instAddGroup {α : Type u_1} [AddGroup α] :
AddGroup (Lex α)
source
@[implicit_reducible]
instance Lex.instCommGroup {α : Type u_1} [CommGroup α] :
CommGroup (Lex α)
source
@[implicit_reducible]
instance Lex.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
AddCommGroup (Lex α)
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 α)
source
@[implicit_reducible]
instance Colex.instZero {α : Type u_1} [Zero α] :
Zero (Colex α)
source
@[implicit_reducible]
instance Colex.instMul {α : Type u_1} [Mul α] :
Mul (Colex α)
source
@[implicit_reducible]
instance Colex.instAdd {α : Type u_1} [Add α] :
Add (Colex α)
source
@[implicit_reducible]
instance Colex.instInv {α : Type u_1} [Inv α] :
Inv (Colex α)
source
@[implicit_reducible]
instance Colex.instNeg {α : Type u_1} [Neg α] :
Neg (Colex α)
source
@[implicit_reducible]
instance Colex.instDiv {α : Type u_1} [Div α] :
Div (Colex α)
source
@[implicit_reducible]
instance Colex.instSub {α : Type u_1} [Sub α] :
Sub (Colex α)
source
@[implicit_reducible]
instance Colex.instPow {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow (Colex α) β
source
@[implicit_reducible]
instance Colex.instSMul {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul β (Colex α)
source
@[implicit_reducible]
instance Colex.instVAdd {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd β (Colex α)
source
@[implicit_reducible]
instance Colex.instPow_1 {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow α (Colex β)
source
@[implicit_reducible]
instance Colex.instSMul' {β : Type u_2} {α : Type u_1} [SMul β α] :
SMul (Colex β) α
source
@[implicit_reducible]
instance Colex.instVAdd' {β : Type u_2} {α : Type u_1} [VAdd β α] :
VAdd (Colex β) α
source
@[implicit_reducible]
instance Colex.instSemigroup {α : Type u_1} [Semigroup α] :
Semigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
CommSemigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
AddCommSemigroup (Colex α)
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 α)
source
@[implicit_reducible]
instance Colex.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
RightCancelSemigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
AddRightCancelSemigroup (Colex α)
source
@[implicit_reducible]
instance Colex.instMulOneClass {α : Type u_1} [MulOneClass α] :
MulOneClass (Colex α)
source
@[implicit_reducible]
instance Colex.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
AddZeroClass (Colex α)
source
@[implicit_reducible]
instance Colex.instMonoid {α : Type u_1} [Monoid α] :
Monoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddMonoid {α : Type u_1} [AddMonoid α] :
AddMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instCommMonoid {α : Type u_1} [CommMonoid α] :
CommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
AddCommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instLeftCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :
LeftCancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddLeftCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :
AddLeftCancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instRightCancelMonoid {α : Type u_1} [RightCancelMonoid α] :
RightCancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddRightCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :
AddRightCancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instCancelMonoid {α : Type u_1} [CancelMonoid α] :
CancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :
AddCancelMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :
CancelCommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :
AddCancelCommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :
InvolutiveInv (Colex α)
source
@[implicit_reducible]
instance Colex.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :
InvolutiveNeg (Colex α)
source
@[implicit_reducible]
instance Colex.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
DivInvMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instSubNegAddMonoid {α : Type u_1} [SubNegMonoid α] :
SubNegMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :
DivisionMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :
SubtractionMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :
DivisionCommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instDivisionAddCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :
SubtractionCommMonoid (Colex α)
source
@[implicit_reducible]
instance Colex.instGroup {α : Type u_1} [Group α] :
Group (Colex α)
source
@[implicit_reducible]
instance Colex.instAddGroup {α : Type u_1} [AddGroup α] :
AddGroup (Colex α)
source
@[implicit_reducible]
instance Colex.instCommGroup {α : Type u_1} [CommGroup α] :
CommGroup (Colex α)
source
@[implicit_reducible]
instance Colex.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
AddCommGroup (Colex α)
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