Equations
- instAddSemigroupOrderDual = h
Equations
- instAddCommSemigroupOrderDual = h
Equations
- instCommSemigroupOrderDual = h
instance
instIsAddLeftCancelOrderDualInstAddOrderDual
{α : Type u_1}
[Add α]
[h : IsLeftCancelAdd α]
:
Equations
- ⋯ = h
instance
instIsLeftCancelMulOrderDualInstMulOrderDual
{α : Type u_1}
[Mul α]
[h : IsLeftCancelMul α]
:
Equations
- ⋯ = h
instance
instIsAddRightCancelOrderDualInstAddOrderDual
{α : Type u_1}
[Add α]
[h : IsRightCancelAdd α]
:
Equations
- ⋯ = h
instance
instIsRightCancelMulOrderDualInstMulOrderDual
{α : Type u_1}
[Mul α]
[h : IsRightCancelMul α]
:
Equations
- ⋯ = h
Equations
- ⋯ = h
Equations
- ⋯ = h
Equations
- instAddLeftCancelSemigroupOrderDual = h
Equations
- instLeftCancelSemigroupOrderDual = h
Equations
- instAddRightCancelSemigroupOrderDual = h
Equations
- instRightCancelSemigroupOrderDual = h
Equations
- instAddZeroClassOrderDual = h
Equations
- instMulOneClassOrderDual = h
Equations
- OrderDual.instAddCommMonoid = h
Equations
- OrderDual.instCommMonoid = h
Equations
- instAddLeftCancelMonoidOrderDual = h
Equations
- instLeftCancelMonoidOrderDual = h
Equations
- instAddRightCancelMonoidOrderDual = h
Equations
- instRightCancelMonoidOrderDual = h
Equations
- instAddCancelMonoidOrderDual = h
Equations
- instCancelMonoidOrderDual = h
Equations
- OrderDual.instAddCancelCommMonoid = h
Equations
- OrderDual.instCancelCommMonoid = 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