Group structure on the order type synonyms #
Transfer algebraic instances from α
to αᵒᵈ
and lex α
.
Equations
- instAddSemigroupOrderDual = h
Equations
- instAddCommSemigroupOrderDual = h
Equations
- instCommSemigroupOrderDual = h
Equations
- instAddLeftCancelSemigroupOrderDual = h
Equations
- instLeftCancelSemigroupOrderDual = h
Equations
- instAddRightCancelSemigroupOrderDual = h
Equations
- instRightCancelSemigroupOrderDual = h
Equations
- instAddZeroClassOrderDual = h
Equations
- instMulOneClassOrderDual = h
Equations
- instAddCommMonoidOrderDual = h
Equations
- instCommMonoidOrderDual = h
Equations
- instAddLeftCancelMonoidOrderDual = h
Equations
- instLeftCancelMonoidOrderDual = h
Equations
- instAddRightCancelMonoidOrderDual = h
Equations
- instRightCancelMonoidOrderDual = h
Equations
- instAddCancelMonoidOrderDual = h
Equations
- instCancelMonoidOrderDual = h
Equations
- instAddCancelCommMonoidOrderDual = h
Equations
- instCancelCommMonoidOrderDual = h
Equations
- instInvolutiveNegOrderDual = h
Equations
- instInvolutiveInvOrderDual = h
Equations
- instSubNegAddMonoidOrderDual = h
Equations
- instDivInvMonoidOrderDual = h
Equations
- OrderDual.subtractionMonoid = h
Equations
- instDivisionMonoidOrderDual = h
Equations
- OrderDual.subtractionCommMonoid = h
Equations
- instDivisionCommMonoidOrderDual = h
Equations
- instAddCommGroupOrderDual = h
Lexicographical order #
Equations
- instAddSemigroupLex = h
Equations
- instAddCommSemigroupLex = h
Equations
- instCommSemigroupLex = h
Equations
- instAddLeftCancelSemigroupLex = h
Equations
- instLeftCancelSemigroupLex = h
Equations
- instAddRightCancelSemigroupLex = h
Equations
- instRightCancelSemigroupLex = h
Equations
- instAddZeroClassLex = h
Equations
- instMulOneClassLex = h
Equations
- instAddCommMonoidLex = h
Equations
- instCommMonoidLex = h
Equations
- instAddLeftCancelMonoidLex = h
Equations
- instLeftCancelMonoidLex = h
Equations
- instAddRightCancelMonoidLex = h
instance
instRightCancelMonoidLex
{α : Type u_1}
[h : RightCancelMonoid α]
:
RightCancelMonoid (Lex α)
Equations
- instRightCancelMonoidLex = h
Equations
- instAddCancelMonoidLex = h
Equations
- instCancelMonoidLex = h
Equations
- instAddCancelCommMonoidLex = h
Equations
- instCancelCommMonoidLex = h
Equations
- instInvolutiveNegLex = h
Equations
- instInvolutiveInvLex = h
Equations
- instSubNegAddMonoidLex = h
Equations
- instDivInvMonoidLex = h
Equations
- instDivisionMonoidLex = h
Equations
- instDivisionCommMonoidLex = h
Equations
- instAddCommGroupLex = h