Group with zero structure on the order type synonyms

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

Order dual

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

Equations

• instMulZeroClassOrderDual = h

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

Equations

• instMulZeroOneClassOrderDual = h

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

Equations

• ⋯ = h

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

Equations

• instSemigroupWithZeroOrderDual = h

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

Equations

• instMonoidWithZeroOrderDual = h

instance instCancelMonoidWithZeroOrderDual {α : Type u_1} [h : CancelMonoidWithZero α] : CancelMonoidWithZero αᵒᵈ

Equations

• instCancelMonoidWithZeroOrderDual = h

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

Equations

• instCommMonoidWithZeroOrderDual = h

instance instCancelCommMonoidWithZeroOrderDual {α : Type u_1} [h : CancelCommMonoidWithZero α] : CancelCommMonoidWithZero αᵒᵈ

Equations

• instCancelCommMonoidWithZeroOrderDual = h

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

Equations

• instGroupWithZeroOrderDual = h

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

Equations

• instCommGroupWithZeroOrderDual = h

Lexicographic order

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

Equations

• instMulZeroClassLex = h

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

Equations

• instMulZeroOneClassLex = h

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

Equations

• ⋯ = h

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

Equations

• instSemigroupWithZeroLex = h

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

Equations

• instMonoidWithZeroLex = h

instance instCancelMonoidWithZeroLex {α : Type u_1} [h : CancelMonoidWithZero α] : CancelMonoidWithZero (Lex α)

Equations

• instCancelMonoidWithZeroLex = h

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

Equations

• instCommMonoidWithZeroLex = h

instance instCancelCommMonoidWithZeroLex {α : Type u_1} [h : CancelCommMonoidWithZero α] : CancelCommMonoidWithZero (Lex α)

Equations

• instCancelCommMonoidWithZeroLex = h

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

Equations

• instGroupWithZeroLex = h

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

Equations

• instCommGroupWithZeroLex = h