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} [MulZeroClass α] : MulZeroClass αᵒᵈ

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

Lexicographic order

@[implicit_reducible]

instance Lex.instMulZeroClass {α : Type u_1} [MulZeroClass α] : MulZeroClass (Lex α)

Equations

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

@[implicit_reducible]

instance Lex.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] : MulZeroOneClass (Lex α)

Equations

• Lex.instMulZeroOneClass = { toMulOneClass := Lex.instMulOneClass, toZero := Lex.instZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Lex.instNoZeroDivisors {α : Type u_1} [Mul α] [Zero α] [NoZeroDivisors α] : NoZeroDivisors (Lex α)

@[implicit_reducible]

instance Lex.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] : SemigroupWithZero (Lex α)

Equations

• Lex.instSemigroupWithZero = { toSemigroup := Lex.instSemigroup, toZero := Lex.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance Lex.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] : MonoidWithZero (Lex α)

Equations

• Lex.instMonoidWithZero = { toMonoid := Lex.instMonoid, toZero := Lex.instZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Lex.instIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] : IsLeftCancelMulZero (Lex α)

instance Lex.instIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] : IsRightCancelMulZero (Lex α)

instance Lex.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsCancelMulZero α] : IsCancelMulZero (Lex α)

@[implicit_reducible]

instance Lex.instCommMonoidWithZero {α : Type u_1} [CommMonoidWithZero α] : CommMonoidWithZero (Lex α)

Equations

• Lex.instCommMonoidWithZero = { toCommMonoid := Lex.instCommMonoid, toZero := Lex.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance Lex.instGroupWithZero {α : Type u_1} [GroupWithZero α] : GroupWithZero (Lex α)

Equations

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

@[implicit_reducible]

instance Lex.instCommGroupWithZero {α : Type u_1} [CommGroupWithZero α] : CommGroupWithZero (Lex α)

Equations

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