Opposites of groups with zero

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] : IsRightCancelMulZero αᵐᵒᵖ

instance MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] : IsLeftCancelMulZero αᵐᵒᵖ

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

@[simp]

theorem MulOpposite.isLeftCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] : IsLeftCancelMulZero αᵐᵒᵖ ↔ IsRightCancelMulZero α

@[simp]

theorem MulOpposite.isRightCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] : IsRightCancelMulZero αᵐᵒᵖ ↔ IsLeftCancelMulZero α

@[simp]

theorem MulOpposite.isCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] : IsCancelMulZero αᵐᵒᵖ ↔ IsCancelMulZero α

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

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