Group with zero structure on the order type synonyms

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

Order dual

@[implicit_reducible]

instance OrderDual.instMulZeroClass {α : Type u_1} [h : MulZeroClass α] : MulZeroClass αᵒᵈ

Equations

• OrderDual.instMulZeroClass = { toMul := OrderDual.instMul, toZero := OrderDual.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance OrderDual.instMulZeroOneClass {α : Type u_1} [h : MulZeroOneClass α] : MulZeroOneClass αᵒᵈ

Equations

• OrderDual.instMulZeroOneClass = { toMulOneClass := OrderDual.instMulOneClass, toZero := OrderDual.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance OrderDual.instNoZeroDivisors {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] : NoZeroDivisors αᵒᵈ

@[implicit_reducible]

instance OrderDual.instSemigroupWithZero {α : Type u_1} [h : SemigroupWithZero α] : SemigroupWithZero αᵒᵈ

Equations

• OrderDual.instSemigroupWithZero = { toSemigroup := OrderDual.instSemigroup, toZero := OrderDual.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance OrderDual.instMonoidWithZero {α : Type u_1} [h : MonoidWithZero α] : MonoidWithZero αᵒᵈ

Equations

• OrderDual.instMonoidWithZero = { toMonoid := OrderDual.instMonoid, toZero := OrderDual.instMulZeroOneClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance OrderDual.instIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [h : IsLeftCancelMulZero α] : IsLeftCancelMulZero αᵒᵈ

instance OrderDual.instIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [h : IsRightCancelMulZero α] : IsRightCancelMulZero αᵒᵈ

instance OrderDual.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [h : IsCancelMulZero α] : IsCancelMulZero αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommMonoidWithZero {α : Type u_1} [h : CommMonoidWithZero α] : CommMonoidWithZero αᵒᵈ

Equations

• OrderDual.instCommMonoidWithZero = { toCommMonoid := OrderDual.instCommMonoid, toZero := OrderDual.instMonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance OrderDual.instGroupWithZero {α : Type u_1} [h : GroupWithZero α] : GroupWithZero αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance OrderDual.instCommGroupWithZero {α : Type u_1} [h : CommGroupWithZero α] : CommGroupWithZero αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

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