Opposites of groups with zero

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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 αᵃᵒᵖ

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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