Opposites of groups with zero

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

Equations

• MulOpposite.instMulZeroClass = MulZeroClass.mk ⋯ ⋯

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

Equations

• MulOpposite.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯

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

Equations

• MulOpposite.instSemigroupWithZero = SemigroupWithZero.mk ⋯ ⋯

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

Equations

• MulOpposite.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

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

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

Equations

• AddOpposite.instMulZeroClass = MulZeroClass.mk ⋯ ⋯

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

Equations

• AddOpposite.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯

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

Equations

• AddOpposite.instSemigroupWithZero = SemigroupWithZero.mk ⋯ ⋯

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

Equations

• AddOpposite.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

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

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

Equations

• AddOpposite.instGroupWithZero = GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯