Group structure on the order type synonyms #
Transfer algebraic instances from α
to αᵒᵈ
, Lex α
, and Colex α
.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Lexicographical order #
Equations
- Lex.instPow = h
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance
instIsRightCancelMulLex
{α : Type u_1}
[Mul α]
[IsRightCancelMul α]
:
IsRightCancelMul (Lex α)
instance
instIsRightCancelAddLex
{α : Type u_1}
[Add α]
[IsRightCancelAdd α]
:
IsRightCancelAdd (Lex α)
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance
instRightCancelMonoidLex
{α : Type u_1}
[h : RightCancelMonoid α]
:
RightCancelMonoid (Lex α)
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance
instSubtractionMonoidLex
{α : Type u_1}
[h : SubtractionMonoid α]
:
SubtractionMonoid (Lex α)
Equations
Equations
Equations
Equations
Equations
Equations
Colexicographical order #
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance
instIsLeftCancelMulColex
{α : Type u_1}
[Mul α]
[IsLeftCancelMul α]
:
IsLeftCancelMul (Colex α)
instance
instIsLeftCancelAddColex
{α : Type u_1}
[Add α]
[IsLeftCancelAdd α]
:
IsLeftCancelAdd (Colex α)