Opposites of groups with zero

instance MulOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] : MulZeroClass αᵐᵒᵖ

Equations

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

instance MulOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ

Equations

• MulOpposite.instMulZeroOneClass = { toMulOneClass := MulOpposite.instMulOneClass, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance MulOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ

Equations

• MulOpposite.instSemigroupWithZero = { toSemigroup := MulOpposite.instSemigroup, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance MulOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ

Equations

• MulOpposite.instMonoidWithZero = { toMonoid := MulOpposite.instMonoid, toZero := MulZeroOneClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance MulOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] : GroupWithZero αᵐᵒᵖ

Equations

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

instance MulOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ

instance AddOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] : MulZeroClass αᵃᵒᵖ

Equations

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

instance AddOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ

Equations

• AddOpposite.instMulZeroOneClass = { toMulOneClass := AddOpposite.instMulOneClass, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance AddOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ

Equations

• AddOpposite.instSemigroupWithZero = { toSemigroup := AddOpposite.instSemigroup, toZero := MulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance AddOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ

Equations

• AddOpposite.instMonoidWithZero = { toMonoid := AddOpposite.instMonoid, toZero := MulZeroOneClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

instance AddOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ

instance AddOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] : GroupWithZero αᵃᵒᵖ

Equations

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