# Opposites of groups with zero #

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

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

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

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

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

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

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

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

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

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

source
instance MulOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] :
NoZeroDivisors α ᵐᵒᵖ
source
instance MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] :
IsRightCancelMulZero α ᵐᵒᵖ
source
instance MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] :
IsLeftCancelMulZero α ᵐᵒᵖ
source
instance MulOpposite.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsCancelMulZero α] :
IsCancelMulZero α ᵐᵒᵖ
source
@[simp]
theorem MulOpposite.isLeftCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
IsLeftCancelMulZero α ᵐᵒᵖ ↔ IsRightCancelMulZero α
source
@[simp]
theorem MulOpposite.isRightCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
IsRightCancelMulZero α ᵐᵒᵖ ↔ IsLeftCancelMulZero α
source
@[simp]
theorem MulOpposite.isCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
IsCancelMulZero α ᵐᵒᵖ ↔ IsCancelMulZero α
source
instance AddOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass α ᵃᵒᵖ
Equations

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

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

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

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

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

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

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

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

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