Group with zero structure on the order type synonyms

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

Order dual

@[implicit_reducible]

instance instMulZeroClassOrderDual {α : Type u_1} [h : MulZeroClass α] : MulZeroClass αᵒᵈ

Equations

• instMulZeroClassOrderDual = h

@[implicit_reducible]

instance instMulZeroOneClassOrderDual {α : Type u_1} [h : MulZeroOneClass α] : MulZeroOneClass αᵒᵈ

Equations

• instMulZeroOneClassOrderDual = h

instance instNoZeroDivisorsOrderDual {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] : NoZeroDivisors αᵒᵈ

@[implicit_reducible]

instance instSemigroupWithZeroOrderDual {α : Type u_1} [h : SemigroupWithZero α] : SemigroupWithZero αᵒᵈ

Equations

• instSemigroupWithZeroOrderDual = h

@[implicit_reducible]

instance instMonoidWithZeroOrderDual {α : Type u_1} [h : MonoidWithZero α] : MonoidWithZero αᵒᵈ

Equations

• instMonoidWithZeroOrderDual = h

instance instIsLeftCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsLeftCancelMulZero α] : IsLeftCancelMulZero αᵒᵈ

instance instIsRightCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsRightCancelMulZero α] : IsRightCancelMulZero αᵒᵈ

instance instIsCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsCancelMulZero α] : IsCancelMulZero αᵒᵈ

@[implicit_reducible]

instance instCommMonoidWithZeroOrderDual {α : Type u_1} [h : CommMonoidWithZero α] : CommMonoidWithZero αᵒᵈ

Equations

• instCommMonoidWithZeroOrderDual = h

@[implicit_reducible]

instance instGroupWithZeroOrderDual {α : Type u_1} [h : GroupWithZero α] : GroupWithZero αᵒᵈ

Equations

• instGroupWithZeroOrderDual = h

@[implicit_reducible]

instance instCommGroupWithZeroOrderDual {α : Type u_1} [h : CommGroupWithZero α] : CommGroupWithZero αᵒᵈ

Equations

• instCommGroupWithZeroOrderDual = h

Lexicographic order

@[implicit_reducible]

instance instMulZeroClassLex {α : Type u_1} [h : MulZeroClass α] : MulZeroClass (Lex α)

Equations

• instMulZeroClassLex = h

@[implicit_reducible]

instance instMulZeroOneClassLex {α : Type u_1} [h : MulZeroOneClass α] : MulZeroOneClass (Lex α)

Equations

• instMulZeroOneClassLex = h

instance instNoZeroDivisorsLex {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] : NoZeroDivisors (Lex α)

@[implicit_reducible]

instance instSemigroupWithZeroLex {α : Type u_1} [h : SemigroupWithZero α] : SemigroupWithZero (Lex α)

Equations

• instSemigroupWithZeroLex = h

@[implicit_reducible]

instance instMonoidWithZeroLex {α : Type u_1} [h : MonoidWithZero α] : MonoidWithZero (Lex α)

Equations

• instMonoidWithZeroLex = h

instance instIsLeftCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsLeftCancelMulZero α] : IsLeftCancelMulZero (Lex α)

instance instIsRightCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsRightCancelMulZero α] : IsRightCancelMulZero (Lex α)

instance instIsCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsCancelMulZero α] : IsCancelMulZero (Lex α)

@[implicit_reducible]

instance instCommMonoidWithZeroLex {α : Type u_1} [h : CommMonoidWithZero α] : CommMonoidWithZero (Lex α)

Equations

• instCommMonoidWithZeroLex = h

@[implicit_reducible]

instance instGroupWithZeroLex {α : Type u_1} [h : GroupWithZero α] : GroupWithZero (Lex α)

Equations

• instGroupWithZeroLex = h

@[implicit_reducible]

instance instCommGroupWithZeroLex {α : Type u_1} [h : CommGroupWithZero α] : CommGroupWithZero (Lex α)

Equations

• instCommGroupWithZeroLex = h