doc-next-gen

Mathlib.Algebra.Order.Group.Synonym

Module docstring

{"# Group structure on the order type synonyms

Transfer algebraic instances from α to αᵒᵈ and Lex α. ","### OrderDual ","### Lexicographical order "}

instOneOrderDual instance
[h : One α] : One αᵒᵈ
Full source 
@[to_additive]
instance [h : One α] : One αᵒᵈ := h
One element operation on order dual
Informal description
For any type $\alpha$ with a one element operation, the order dual $\alpha^{\text{op}}$ also has a one element operation.
instMulOrderDual instance
[h : Mul α] : Mul αᵒᵈ
Full source 
@[to_additive]
instance [h : Mul α] : Mul αᵒᵈ := h
Multiplication on Order Duals
Informal description
For any type $\alpha$ equipped with a multiplication operation, the order dual $\alpha^{\text{op}}$ also inherits a multiplication operation.
instInvOrderDual instance
[h : Inv α] : Inv αᵒᵈ
Full source 
@[to_additive]
instance [h : Inv α] : Inv αᵒᵈ := h
Inversion Operation on Order Dual
Informal description
For any type $\alpha$ with an inversion operation, the order dual $\alpha^{\text{op}}$ also has an inversion operation.
instDivOrderDual instance
[h : Div α] : Div αᵒᵈ
Full source 
@[to_additive]
instance [h : Div α] : Div αᵒᵈ := h
Division Operation on Order Dual
Informal description
For any type $\alpha$ equipped with a division operation, the order dual $\alpha^{\text{op}}$ also inherits a division operation.
OrderDual.instPow instance
[h : Pow α β] : Pow αᵒᵈ β
Full source 
@[to_additive (attr := to_additive) (reorder := 1 2) OrderDual.instSMul]
instance OrderDual.instPow [h : Pow α β] : Pow αᵒᵈ β := h
Power Operation on Order Dual
Informal description
For any type $\alpha$ equipped with a power operation $\alpha \times \beta \to \alpha$, the order dual $\alpha^\text{op}$ also inherits a power operation.
OrderDual.instPow' instance
[h : Pow α β] : Pow α βᵒᵈ
Full source 
@[to_additive (attr := to_additive) (reorder := 1 2) OrderDual.instSMul']
instance OrderDual.instPow' [h : Pow α β] : Pow α βᵒᵈ := h
Power Operation on Order Dual of Exponent
Informal description
For any types $\alpha$ and $\beta$ with a power operation $\alpha^\beta$, there is a power operation $\alpha^{\beta^{\text{op}}}$ where $\beta^{\text{op}}$ is the order dual of $\beta$.
instSemigroupOrderDual instance
[h : Semigroup α] : Semigroup αᵒᵈ
Full source 
@[to_additive]
instance [h : Semigroup α] : Semigroup αᵒᵈ := h
Semigroup Structure on Order Dual
Informal description
For any semigroup $\alpha$, the order dual $\alpha^{\text{op}}$ is also a semigroup.
instCommSemigroupOrderDual instance
[h : CommSemigroup α] : CommSemigroup αᵒᵈ
Full source 
@[to_additive]
instance [h : CommSemigroup α] : CommSemigroup αᵒᵈ := h
Commutative Semigroup Structure on Order Dual
Informal description
For any commutative semigroup $\alpha$, the order dual $\alpha^{\text{op}}$ is also a commutative semigroup.
instIsLeftCancelMulOrderDual instance
[Mul α] [h : IsLeftCancelMul α] : IsLeftCancelMul αᵒᵈ
Full source 
@[to_additive]
instance [Mul α] [h : IsLeftCancelMul α] : IsLeftCancelMul αᵒᵈ := h
Left Cancellation Property on Order Duals
Informal description
For any type $\alpha$ with a multiplication operation that satisfies the left cancellation property (i.e., $a \cdot b = a \cdot c$ implies $b = c$ for all $a, b, c \in \alpha$), the order dual $\alpha^{\text{op}}$ also satisfies the left cancellation property.
instIsRightCancelMulOrderDual instance
[Mul α] [h : IsRightCancelMul α] : IsRightCancelMul αᵒᵈ
Full source 
@[to_additive]
instance [Mul α] [h : IsRightCancelMul α] : IsRightCancelMul αᵒᵈ := h
Right Cancellative Multiplication on Order Duals
Informal description
For any type $\alpha$ with a multiplication operation that is right cancellative, the order dual $\alpha^{\text{op}}$ is also right cancellative.
instIsCancelMulOrderDual instance
[Mul α] [h : IsCancelMul α] : IsCancelMul αᵒᵈ
Full source 
@[to_additive]
instance [Mul α] [h : IsCancelMul α] : IsCancelMul αᵒᵈ := h
Cancellative Multiplication on Order Duals
Informal description
For any type $\alpha$ with a multiplication operation that is both left and right cancellative, the order dual $\alpha^{\text{op}}$ also inherits a cancellative multiplication operation.
instLeftCancelSemigroupOrderDual instance
[h : LeftCancelSemigroup α] : LeftCancelSemigroup αᵒᵈ
Full source 
@[to_additive]
instance [h : LeftCancelSemigroup α] : LeftCancelSemigroup αᵒᵈ := h
Order Dual of a Left Cancellative Semigroup is Left Cancellative
Informal description
For any left cancellative semigroup $\alpha$, the order dual $\alpha^{\text{op}}$ is also a left cancellative semigroup.
instRightCancelSemigroupOrderDual instance
[h : RightCancelSemigroup α] : RightCancelSemigroup αᵒᵈ
Full source 
@[to_additive]
instance [h : RightCancelSemigroup α] : RightCancelSemigroup αᵒᵈ := h
Order Dual of a Right Cancellative Semigroup is Right Cancellative
Informal description
For any right cancellative semigroup $\alpha$, the order dual $\alpha^{\text{op}}$ is also a right cancellative semigroup.
instMulOneClassOrderDual instance
[h : MulOneClass α] : MulOneClass αᵒᵈ
Full source 
@[to_additive]
instance [h : MulOneClass α] : MulOneClass αᵒᵈ := h
Multiplication and Identity Structure on Order Duals
Informal description
For any type $\alpha$ with a multiplication operation and a multiplicative identity (i.e., a `MulOneClass` structure), the order dual $\alpha^{\text{op}}$ also inherits a `MulOneClass` structure.
instMonoidOrderDual instance
[h : Monoid α] : Monoid αᵒᵈ
Full source 
@[to_additive]
instance [h : Monoid α] : Monoid αᵒᵈ := h
Monoid Structure on Order Dual
Informal description
For any monoid $\alpha$, the order dual $\alpha^{\mathrm{op}}$ is also a monoid.
OrderDual.instCommMonoid instance
[h : CommMonoid α] : CommMonoid αᵒᵈ
Full source 
@[to_additive]
instance OrderDual.instCommMonoid [h : CommMonoid α] : CommMonoid αᵒᵈ := h
Order Dual of a Commutative Monoid is a Commutative Monoid
Informal description
For any commutative monoid $\alpha$, the order dual $\alpha^{\text{op}}$ is also a commutative monoid.
instLeftCancelMonoidOrderDual instance
[h : LeftCancelMonoid α] : LeftCancelMonoid αᵒᵈ
Full source 
@[to_additive]
instance [h : LeftCancelMonoid α] : LeftCancelMonoid αᵒᵈ := h
Order Dual of a Left Cancelative Monoid is a Left Cancelative Monoid
Informal description
For any left cancelative monoid $\alpha$, the order dual $\alpha^{\text{op}}$ is also a left cancelative monoid.
instRightCancelMonoidOrderDual instance
[h : RightCancelMonoid α] : RightCancelMonoid αᵒᵈ
Full source 
@[to_additive]
instance [h : RightCancelMonoid α] : RightCancelMonoid αᵒᵈ := h
Order Dual of a Right Cancelative Monoid is a Right Cancelative Monoid
Informal description
For any right cancelative monoid $\alpha$, the order dual $\alpha^{\text{op}}$ is also a right cancelative monoid.
instCancelMonoidOrderDual instance
[h : CancelMonoid α] : CancelMonoid αᵒᵈ
Full source 
@[to_additive]
instance [h : CancelMonoid α] : CancelMonoid αᵒᵈ := h
Cancel Monoid Structure on Order Dual
Informal description
For any type $\alpha$ with a cancel monoid structure, the order dual $\alpha^{\text{op}}$ also inherits a cancel monoid structure.
OrderDual.instCancelCommMonoid instance
[h : CancelCommMonoid α] : CancelCommMonoid αᵒᵈ
Full source 
@[to_additive]
instance OrderDual.instCancelCommMonoid [h : CancelCommMonoid α] : CancelCommMonoid αᵒᵈ := h
Cancelative Commutative Monoid Structure on Order Duals
Informal description
For any type $\alpha$ with a cancelative commutative monoid structure, the order dual $\alpha^{\text{op}}$ also inherits a cancelative commutative monoid structure.
instInvolutiveInvOrderDual instance
[h : InvolutiveInv α] : InvolutiveInv αᵒᵈ
Full source 
@[to_additive]
instance [h : InvolutiveInv α] : InvolutiveInv αᵒᵈ := h
Involutive Inversion on Order Duals
Informal description
For any type $\alpha$ with an involutive inversion operation, the order dual $\alpha^{\text{op}}$ also has an involutive inversion operation.
instDivInvMonoidOrderDual instance
[h : DivInvMonoid α] : DivInvMonoid αᵒᵈ
Full source 
@[to_additive]
instance [h : DivInvMonoid α] : DivInvMonoid αᵒᵈ := h
Division Monoid Structure on Order Dual
Informal description
For any type $\alpha$ with a division monoid structure, the order dual $\alpha^{\text{op}}$ also inherits a division monoid structure.
instDivisionMonoidOrderDual instance
[h : DivisionMonoid α] : DivisionMonoid αᵒᵈ
Full source 
@[to_additive]
instance [h : DivisionMonoid α] : DivisionMonoid αᵒᵈ := h
Order Dual of a Division Monoid is a Division Monoid
Informal description
For any division monoid $\alpha$, the order dual $\alpha^{\text{op}}$ is also a division monoid.
instDivisionCommMonoidOrderDual instance
[h : DivisionCommMonoid α] : DivisionCommMonoid αᵒᵈ
Full source 
@[to_additive OrderDual.subtractionCommMonoid]
instance [h : DivisionCommMonoid α] : DivisionCommMonoid αᵒᵈ := h
Order Dual of a Division Commutative Monoid is a Division Commutative Monoid
Informal description
For any division commutative monoid $\alpha$, the order dual $\alpha^{\text{op}}$ is also a division commutative monoid.
OrderDual.instGroup instance
[h : Group α] : Group αᵒᵈ
Full source 
@[to_additive]
instance OrderDual.instGroup [h : Group α] : Group αᵒᵈ := h
Group Structure on Order Dual
Informal description
For any group $\alpha$, the order dual $\alpha^{\text{op}}$ is also a group.
instCommGroupOrderDual instance
[h : CommGroup α] : CommGroup αᵒᵈ
Full source 
@[to_additive]
instance [h : CommGroup α] : CommGroup αᵒᵈ := h
Order Dual of a Commutative Group is a Commutative Group
Informal description
For any commutative group $\alpha$, the order dual $\alpha^{\text{op}}$ is also a commutative group.
toDual_one theorem
[One α] : toDual (1 : α) = 1
Full source 
@[to_additive (attr := simp)]
theorem toDual_one [One α] : toDual (1 : α) = 1 := rfl
Identity Preservation under Order Dualization
Informal description
For any type $\alpha$ with a multiplicative identity element $1$, the order dual of $1$ is equal to $1$ in the order dual type $\alpha^{\text{op}}$, i.e., $\text{toDual}(1) = 1$.
ofDual_one theorem
[One α] : (ofDual 1 : α) = 1
Full source 
@[to_additive (attr := simp)]
theorem ofDual_one [One α] : (ofDual 1 : α) = 1 := rfl
Identity Preservation under Order Dual Conversion
Informal description
For any type $\alpha$ with a multiplicative identity element $1$, the conversion of $1$ from the order dual $\alpha^{\text{op}}$ back to $\alpha$ preserves the identity, i.e., $\text{ofDual}(1) = 1$.
toDual_mul theorem
[Mul α] (a b : α) : toDual (a * b) = toDual a * toDual b
Full source 
@[to_additive (attr := simp)]
theorem toDual_mul [Mul α] (a b : α) : toDual (a * b) = toDual a * toDual b := rfl
Multiplication Preserved under Order Dualization
Informal description
For any type $\alpha$ with a multiplication operation and any elements $a, b \in \alpha$, the order dual of the product $a \cdot b$ is equal to the product of the order duals of $a$ and $b$, i.e., $\text{toDual}(a \cdot b) = \text{toDual}(a) \cdot \text{toDual}(b)$.
ofDual_mul theorem
[Mul α] (a b : αᵒᵈ) : ofDual (a * b) = ofDual a * ofDual b
Full source 
@[to_additive (attr := simp)]
theorem ofDual_mul [Mul α] (a b : αᵒᵈ) : ofDual (a * b) = ofDual a * ofDual b := rfl
Multiplication Commutes with Order Dual Conversion
Informal description
For any type $\alpha$ with a multiplication operation and any elements $a, b$ in the order dual $\alpha^{\text{op}}$, the operation of converting back to $\alpha$ commutes with multiplication, i.e., $\text{ofDual}(a \cdot b) = \text{ofDual}(a) \cdot \text{ofDual}(b)$.
toDual_inv theorem
[Inv α] (a : α) : toDual a⁻¹ = (toDual a)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem toDual_inv [Inv α] (a : α) : toDual a⁻¹ = (toDual a)⁻¹ := rfl
Inversion Commutes with Order Dualization
Informal description
For any type $\alpha$ with an inversion operation and any element $a \in \alpha$, the order dual of the inverse of $a$ is equal to the inverse of the order dual of $a$, i.e., $\text{toDual}(a^{-1}) = (\text{toDual}(a))^{-1}$.
ofDual_inv theorem
[Inv α] (a : αᵒᵈ) : ofDual a⁻¹ = (ofDual a)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem ofDual_inv [Inv α] (a : αᵒᵈ) : ofDual a⁻¹ = (ofDual a)⁻¹ := rfl
Inversion Commutes with Order Dual Conversion
Informal description
For any type $\alpha$ with an inversion operation and any element $a$ in the order dual $\alpha^{\text{op}}$, the operation of converting back to $\alpha$ commutes with inversion, i.e., $\text{ofDual}(a^{-1}) = (\text{ofDual}(a))^{-1}$.
toDual_div theorem
[Div α] (a b : α) : toDual (a / b) = toDual a / toDual b
Full source 
@[to_additive (attr := simp)]
theorem toDual_div [Div α] (a b : α) : toDual (a / b) = toDual a / toDual b := rfl
Division Preserved Under Order Dualization
Informal description
For any type $\alpha$ equipped with a division operation and any elements $a, b \in \alpha$, the order dual of the quotient $a / b$ is equal to the quotient of the order duals of $a$ and $b$, i.e., $\text{toDual}(a / b) = \text{toDual}(a) / \text{toDual}(b)$.
ofDual_div theorem
[Div α] (a b : αᵒᵈ) : ofDual (a / b) = ofDual a / ofDual b
Full source 
@[to_additive (attr := simp)]
theorem ofDual_div [Div α] (a b : αᵒᵈ) : ofDual (a / b) = ofDual a / ofDual b := rfl
Division Compatibility with Order Dual Conversion: $\text{ofDual}(a / b) = \text{ofDual}(a) / \text{ofDual}(b)$
Informal description
For any type $\alpha$ equipped with a division operation and any elements $a, b$ in the order dual $\alpha^{\text{op}}$, the conversion of the quotient $a / b$ back to $\alpha$ equals the quotient of the converted elements, i.e., $\text{ofDual}(a / b) = \text{ofDual}(a) / \text{ofDual}(b)$.
toDual_pow theorem
[Pow α β] (a : α) (b : β) : toDual (a ^ b) = toDual a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toDual_smul]
theorem toDual_pow [Pow α β] (a : α) (b : β) : toDual (a ^ b) = toDual a ^ b := rfl
Power Operation Preserved Under Order Dual
Informal description
For any type $\alpha$ with a power operation $\alpha \times \beta \to \alpha$ and any elements $a \in \alpha$, $b \in \beta$, the order dual of $a^b$ equals the power of the order dual of $a$ with exponent $b$, i.e., $\text{toDual}(a^b) = (\text{toDual}\, a)^b$.
ofDual_pow theorem
[Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofDual_smul]
theorem ofDual_pow [Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b := rfl
Power Operation Compatibility with Order Dual Conversion: $\text{ofDual}(a^b) = (\text{ofDual}\, a)^b$
Informal description
For any type $\alpha$ equipped with a power operation $\alpha \times \beta \to \alpha$ and any elements $a \in \alpha^\text{op}$, $b \in \beta$, the conversion of $a^b$ back to $\alpha$ equals the power of the converted element $\text{ofDual}\, a$ with exponent $b$, i.e., $\text{ofDual}(a^b) = (\text{ofDual}\, a)^b$.
pow_toDual theorem
[Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toDual_smul']
theorem pow_toDual [Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b := rfl
Power Operation Invariance Under Order Dual of Exponent
Informal description
For any type $\alpha$ with a power operation $\alpha^\beta$ and any elements $a \in \alpha$, $b \in \beta$, the power $a^{\text{toDual}\, b}$ is equal to $a^b$.
pow_ofDual theorem
[Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofDual_smul']
theorem pow_ofDual [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b := rfl
Power Operation Invariance Under Order Dual Conversion: $a^{\text{ofDual}\, b} = a^b$
Informal description
For any type $\alpha$ with a power operation $\alpha^\beta$ and any elements $a \in \alpha$, $b \in \beta^\text{op}$, the power $a^{\text{ofDual}\, b}$ is equal to $a^b$.
instOneLex instance
[h : One α] : One (Lex α)
Full source 
@[to_additive]
instance [h : One α] : One (Lex α) := h
One Element in Lexicographic Order
Informal description
For any type $\alpha$ with a one element $1$, the lexicographic order on $\alpha$ also has a one element.
instMulLex instance
[h : Mul α] : Mul (Lex α)
Full source 
@[to_additive]
instance [h : Mul α] : Mul (Lex α) := h
Multiplication on Lexicographically Ordered Types
Informal description
For any type $\alpha$ equipped with a multiplication operation, the lexicographic order on $\alpha$ inherits a multiplication operation defined componentwise.
instInvLex instance
[h : Inv α] : Inv (Lex α)
Full source 
@[to_additive]
instance [h : Inv α] : Inv (Lex α) := h
Inversion Operation on Lexicographic Order
Informal description
For any type $\alpha$ with an inversion operation $x \mapsto x^{-1}$, the lexicographic order on $\alpha$ also inherits an inversion operation.
instDivLex instance
[h : Div α] : Div (Lex α)
Full source 
@[to_additive]
instance [h : Div α] : Div (Lex α) := h
Division Operation on Lexicographically Ordered Types
Informal description
For any type $\alpha$ equipped with a division operation, the lexicographical order on $\alpha$ inherits a division operation.
Lex.instPow instance
[h : Pow α β] : Pow (Lex α) β
Full source 
@[to_additive (attr := to_additive) (reorder := 1 2) Lex.instSMul]
instance Lex.instPow [h : Pow α β] : Pow (Lex α) β := h
Power Operation on Lexicographically Ordered Base
Informal description
For any types $\alpha$ and $\beta$ equipped with a power operation $\alpha^\beta$, the lexicographical order on $\alpha$ induces a power operation on $\alpha$ in lexicographical order with exponent $\beta$.
Lex.instPow' instance
[h : Pow α β] : Pow α (Lex β)
Full source 
@[to_additive (attr := to_additive) (reorder := 1 2) Lex.instSMul']
instance Lex.instPow' [h : Pow α β] : Pow α (Lex β) := h
Power Operation with Lexicographical Exponent
Informal description
For any types $\alpha$ and $\beta$ equipped with a power operation $\alpha^\beta$, the lexicographical order on $\beta$ induces a power operation on $\alpha$ with exponent $\beta$ in lexicographical order.
instSemigroupLex instance
[h : Semigroup α] : Semigroup (Lex α)
Full source 
@[to_additive]
instance [h : Semigroup α] : Semigroup (Lex α) := h
Semigroup Structure on Lexicographical Order
Informal description
For any semigroup $\alpha$, the lexicographical order on $\alpha$ inherits a semigroup structure.
instCommSemigroupLex instance
[h : CommSemigroup α] : CommSemigroup (Lex α)
Full source 
@[to_additive]
instance [h : CommSemigroup α] : CommSemigroup (Lex α) := h
Commutative Semigroup Structure on Lexicographical Order
Informal description
For any commutative semigroup $\alpha$, the lexicographical order on $\alpha$ also forms a commutative semigroup.
instIsLeftCancelMulLex instance
[Mul α] [IsLeftCancelMul α] : IsLeftCancelMul (Lex α)
Full source 
@[to_additive]
instance [Mul α] [IsLeftCancelMul α] : IsLeftCancelMul (Lex α) :=
  inferInstanceAs <| IsLeftCancelMul α
Left Cancellation Property in Lexicographical Order
Informal description
For any type $\alpha$ with a multiplication operation that satisfies the left cancellation property (i.e., $a \cdot b = a \cdot c$ implies $b = c$ for all $a, b, c \in \alpha$), the lexicographical order on $\alpha$ also inherits the left cancellation property for multiplication.
instIsRightCancelMulLex instance
[Mul α] [IsRightCancelMul α] : IsRightCancelMul (Lex α)
Full source 
@[to_additive]
instance [Mul α] [IsRightCancelMul α] : IsRightCancelMul (Lex α) :=
  inferInstanceAs <| IsRightCancelMul α
Right Cancellation Property in Lexicographical Order
Informal description
For any type $\alpha$ with a multiplication operation that satisfies the right cancellation property (i.e., $b \cdot a = c \cdot a$ implies $b = c$ for all $a, b, c \in \alpha$), the lexicographical order on $\alpha$ also inherits the right cancellation property for multiplication.
instIsCancelMulLex instance
[Mul α] [IsCancelMul α] : IsCancelMul (Lex α)
Full source 
@[to_additive]
instance [Mul α] [IsCancelMul α] : IsCancelMul (Lex α) :=
  inferInstanceAs <| IsCancelMul α
Cancellative Multiplication in Lexicographical Order
Informal description
For any type $\alpha$ with a multiplication operation that satisfies both left and right cancellation properties (i.e., $a \cdot b = a \cdot c$ implies $b = c$ and $b \cdot a = c \cdot a$ implies $b = c$ for all $a, b, c \in \alpha$), the lexicographical order on $\alpha$ also inherits these cancellation properties for multiplication.
instLeftCancelSemigroupLex instance
[h : LeftCancelSemigroup α] : LeftCancelSemigroup (Lex α)
Full source 
@[to_additive]
instance [h : LeftCancelSemigroup α] : LeftCancelSemigroup (Lex α) := h
Lexicographical Order Preserves Left-Cancellative Semigroup Structure
Informal description
For any left-cancellative semigroup $\alpha$, the lexicographical order on $\alpha$ also forms a left-cancellative semigroup.
instRightCancelSemigroupLex instance
[h : RightCancelSemigroup α] : RightCancelSemigroup (Lex α)
Full source 
@[to_additive]
instance [h : RightCancelSemigroup α] : RightCancelSemigroup (Lex α) := h
Right-Cancellative Semigroup Structure on Lexicographical Order
Informal description
For any right-cancellative semigroup $\alpha$, the lexicographical order on $\alpha$ also forms a right-cancellative semigroup.
instMulOneClassLex instance
[h : MulOneClass α] : MulOneClass (Lex α)
Full source 
@[to_additive]
instance [h : MulOneClass α] : MulOneClass (Lex α) := h
Multiplication and Identity Structure on Lexicographic Order
Informal description
For any type $\alpha$ with a multiplication and identity element (i.e., a `MulOneClass` structure), the lexicographic order on $\alpha$ (denoted `Lex α`) inherits the same `MulOneClass` structure.
instMonoidLex instance
[h : Monoid α] : Monoid (Lex α)
Full source 
@[to_additive]
instance [h : Monoid α] : Monoid (Lex α) := h
Monoid Structure on Lexicographical Order
Informal description
For any monoid $\alpha$, the lexicographical order on $\alpha$ also forms a monoid with the same multiplication and identity element.
instCommMonoidLex instance
[h : CommMonoid α] : CommMonoid (Lex α)
Full source 
@[to_additive]
instance [h : CommMonoid α] : CommMonoid (Lex α) := h
Commutative Monoid Structure on Lexicographical Order
Informal description
For any commutative monoid $\alpha$, the lexicographical order on $\alpha$ also forms a commutative monoid.
instLeftCancelMonoidLex instance
[h : LeftCancelMonoid α] : LeftCancelMonoid (Lex α)
Full source 
@[to_additive]
instance [h : LeftCancelMonoid α] : LeftCancelMonoid (Lex α) := h
Lexicographic Order Preserves Left-Cancelative Monoid Structure
Informal description
For any left-cancelative monoid $\alpha$, the lexicographic order on $\alpha$ also forms a left-cancelative monoid.
instRightCancelMonoidLex instance
[h : RightCancelMonoid α] : RightCancelMonoid (Lex α)
Full source 
@[to_additive]
instance [h : RightCancelMonoid α] : RightCancelMonoid (Lex α) := h
Right-Cancelative Monoid Structure on Lexicographic Order
Informal description
For any right-cancelative monoid $\alpha$, the lexicographic order on $\alpha$ also forms a right-cancelative monoid.
instCancelMonoidLex instance
[h : CancelMonoid α] : CancelMonoid (Lex α)
Full source 
@[to_additive]
instance [h : CancelMonoid α] : CancelMonoid (Lex α) := h
Lexicographical Order Preserves Cancel Monoid Structure
Informal description
For any type $\alpha$ with a cancel monoid structure, the lexicographical order on $\alpha$ also forms a cancel monoid.
instCancelCommMonoidLex instance
[h : CancelCommMonoid α] : CancelCommMonoid (Lex α)
Full source 
@[to_additive]
instance [h : CancelCommMonoid α] : CancelCommMonoid (Lex α) := h
Cancelative Commutative Monoid Structure on Lexicographic Order
Informal description
For any type $\alpha$ with a cancelative commutative monoid structure, the lexicographic order on $\alpha$ also inherits a cancelative commutative monoid structure.
instInvolutiveInvLex instance
[h : InvolutiveInv α] : InvolutiveInv (Lex α)
Full source 
@[to_additive]
instance [h : InvolutiveInv α] : InvolutiveInv (Lex α) := h
Involutive Inversion on Lexicographical Order
Informal description
For any type $\alpha$ with an involutive inversion operation, the lexicographical order on $\alpha$ also inherits an involutive inversion operation.
instDivInvMonoidLex instance
[h : DivInvMonoid α] : DivInvMonoid (Lex α)
Full source 
@[to_additive]
instance [h : DivInvMonoid α] : DivInvMonoid (Lex α) := h
Division-Inverse Monoid Structure on Lexicographical Order
Informal description
For any type $\alpha$ with a division-inverse monoid structure, the lexicographical order on $\alpha$ also inherits a division-inverse monoid structure.
instDivisionMonoidLex instance
[h : DivisionMonoid α] : DivisionMonoid (Lex α)
Full source 
@[to_additive]
instance [h : DivisionMonoid α] : DivisionMonoid (Lex α) := h
Lexicographical Order Preserves Division Monoid Structure
Informal description
For any division monoid $\alpha$, the lexicographical order on $\alpha$ also forms a division monoid.
instDivisionCommMonoidLex instance
[h : DivisionCommMonoid α] : DivisionCommMonoid (Lex α)
Full source 
@[to_additive existing OrderDual.subtractionCommMonoid]
instance [h : DivisionCommMonoid α] : DivisionCommMonoid (Lex α) := h
Division Commutative Monoid Structure on Lexicographical Order
Informal description
For any type $\alpha$ with a division commutative monoid structure, the lexicographical order on $\alpha$ also inherits a division commutative monoid structure.
instGroupLex instance
[h : Group α] : Group (Lex α)
Full source 
@[to_additive]
instance [h : Group α] : Group (Lex α) := h
Group Structure on Lexicographical Order
Informal description
For any group $\alpha$, the lexicographical order on $\alpha$ also forms a group.
instCommGroupLex instance
[h : CommGroup α] : CommGroup (Lex α)
Full source 
@[to_additive]
instance [h : CommGroup α] : CommGroup (Lex α) := h
Commutative Group Structure on Lexicographic Order
Informal description
For any commutative group $\alpha$, the lexicographic order on $\alpha$ also forms a commutative group.
toLex_one theorem
[One α] : toLex (1 : α) = 1
Full source 
@[to_additive (attr := simp)]
theorem toLex_one [One α] : toLex (1 : α) = 1 := rfl
Preservation of Multiplicative Identity under Lexicographic Order Embedding
Informal description
For any type $\alpha$ with a multiplicative identity element $1$, the embedding `toLex` from $\alpha$ to its lexicographic order `Lex α` maps $1$ to the multiplicative identity in `Lex α$, i.e., $\text{toLex}(1) = 1$.
ofLex_one theorem
[One α] : (ofLex 1 : α) = 1
Full source 
@[to_additive (attr := simp)]
theorem ofLex_one [One α] : (ofLex 1 : α) = 1 := rfl
Preservation of Multiplicative Identity under Lexicographic Order Projection
Informal description
For any type $\alpha$ with a multiplicative identity element $1$, the projection `ofLex` from the lexicographic order `Lex α` back to $\alpha$ maps the multiplicative identity in `Lex α` to $1$ in $\alpha$, i.e., $\text{ofLex}(1) = 1$.
toLex_mul theorem
[Mul α] (a b : α) : toLex (a * b) = toLex a * toLex b
Full source 
@[to_additive (attr := simp)]
theorem toLex_mul [Mul α] (a b : α) : toLex (a * b) = toLex a * toLex b := rfl
Multiplication Preservation under Lexicographic Order Embedding
Informal description
For any type $\alpha$ equipped with a multiplication operation, the map `toLex` from $\alpha$ to its lexicographic order `Lex α` preserves multiplication. That is, for any $a, b \in \alpha$, we have $\text{toLex}(a * b) = \text{toLex}(a) * \text{toLex}(b)$.
ofLex_mul theorem
[Mul α] (a b : Lex α) : ofLex (a * b) = ofLex a * ofLex b
Full source 
@[to_additive (attr := simp)]
theorem ofLex_mul [Mul α] (a b : Lex α) : ofLex (a * b) = ofLex a * ofLex b := rfl
Multiplication Preservation under Lexicographic Order Projection
Informal description
For any type $\alpha$ equipped with a multiplication operation, the projection `ofLex` from the lexicographic order `Lex α` back to $\alpha$ preserves multiplication. That is, for any $a, b \in \text{Lex}\,\alpha$, we have $\text{ofLex}(a * b) = \text{ofLex}(a) * \text{ofLex}(b)$.
toLex_inv theorem
[Inv α] (a : α) : toLex a⁻¹ = (toLex a)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem toLex_inv [Inv α] (a : α) : toLex a⁻¹ = (toLex a)⁻¹ := rfl
Preservation of Inversion under Lexicographic Order Embedding
Informal description
For any type $\alpha$ with an inversion operation $x \mapsto x^{-1}$, the map `toLex` from $\alpha$ to its lexicographic order `Lex α` preserves inversion. That is, for any $a \in \alpha$, we have $\text{toLex}(a^{-1}) = (\text{toLex}(a))^{-1}$.
ofLex_inv theorem
[Inv α] (a : Lex α) : ofLex a⁻¹ = (ofLex a)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem ofLex_inv [Inv α] (a : Lex α) : ofLex a⁻¹ = (ofLex a)⁻¹ := rfl
Inversion Commutes with Lexicographic Order Projection: $\text{ofLex}(a^{-1}) = (\text{ofLex}(a))^{-1}$
Informal description
For any type $\alpha$ with an inversion operation $x \mapsto x^{-1}$, and for any element $a$ in the lexicographic order `Lex α`, the projection `ofLex` satisfies $\text{ofLex}(a^{-1}) = (\text{ofLex}(a))^{-1}$.
toLex_div theorem
[Div α] (a b : α) : toLex (a / b) = toLex a / toLex b
Full source 
@[to_additive (attr := simp)]
theorem toLex_div [Div α] (a b : α) : toLex (a / b) = toLex a / toLex b := rfl
Lexicographical Order Preserves Division: $\text{toLex}(a / b) = \text{toLex}(a) / \text{toLex}(b)$
Informal description
For any type $\alpha$ equipped with a division operation, and for any elements $a, b \in \alpha$, the lexicographical order embedding of $a / b$ is equal to the division of the lexicographical order embeddings of $a$ and $b$, i.e., $\text{toLex}(a / b) = \text{toLex}(a) / \text{toLex}(b)$.
ofLex_div theorem
[Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b
Full source 
@[to_additive (attr := simp)]
theorem ofLex_div [Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b := rfl
Division Commutes with Lexicographical Order Projection
Informal description
For any type $\alpha$ equipped with a division operation, and for any elements $a$ and $b$ in the lexicographical order on $\alpha$, the underlying value of $a / b$ in $\alpha$ is equal to the division of the underlying values of $a$ and $b$. That is, $\text{ofLex}(a / b) = \text{ofLex}(a) / \text{ofLex}(b)$.
toLex_pow theorem
[Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toLex_smul]
theorem toLex_pow [Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b := rfl
Power Operation Preserved Under Lexicographical Order Embedding
Informal description
For any types $\alpha$ and $\beta$ equipped with a power operation $\alpha^\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, the lexicographical order embedding of $a^b$ equals the power of the lexicographical order embedding of $a$ with exponent $b$. That is, $\text{toLex}(a^b) = \text{toLex}(a)^b$.
ofLex_pow theorem
[Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul]
theorem ofLex_pow [Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b := rfl
Power Operation Commutes with Lexicographical Order Projection
Informal description
For any types $\alpha$ and $\beta$ with a power operation $\alpha^\beta$, and for any element $a$ in the lexicographical order on $\alpha$ and any element $b$ in $\beta$, the underlying value of $a^b$ in $\alpha$ is equal to the underlying value of $a$ raised to the power of $b$. That is, $\text{ofLex}(a^b) = \text{ofLex}(a)^b$.
pow_toLex theorem
[Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toLex_smul']
theorem pow_toLex [Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b := rfl
Power Operation Invariance Under Lexicographical Order Embedding in Exponent
Informal description
For any types $\alpha$ and $\beta$ equipped with a power operation $\alpha^\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, the power of $a$ with exponent $\text{toLex}(b)$ is equal to the power of $a$ with exponent $b$. That is, $a^{\text{toLex}(b)} = a^b$.
pow_ofLex theorem
[Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b
Full source 
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul']
theorem pow_ofLex [Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b := rfl
Power Operation Commutes with Lexicographical Order Projection in Exponent
Informal description
For any types $\alpha$ and $\beta$ with a power operation $\alpha^\beta$, and for any element $a \in \alpha$ and any element $b$ in the lexicographical order on $\beta$, we have $a^{\text{ofLex}(b)} = a^b$.