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 = let __spread.0 := MulOpposite.instMulOneClass; let __spread.1 := MulOpposite.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯

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

Equations

• MulOpposite.instSemigroupWithZero = let __spread.0 := MulOpposite.instSemigroup; let __spread.1 := MulOpposite.instMulZeroClass; SemigroupWithZero.mk ⋯ ⋯

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

Equations

• MulOpposite.instMonoidWithZero = let __spread.0 := MulOpposite.instMonoid; let __spread.1 := MulOpposite.instMulZeroOneClass; MonoidWithZero.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• AddOpposite.instMulZeroClass = MulZeroClass.mk ⋯ ⋯

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

Equations

• AddOpposite.instMulZeroOneClass = let __spread.0 := AddOpposite.instMulOneClass; let __spread.1 := AddOpposite.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯

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

Equations

• AddOpposite.instSemigroupWithZero = let __spread.0 := AddOpposite.instSemigroup; let __spread.1 := AddOpposite.instMulZeroClass; SemigroupWithZero.mk ⋯ ⋯

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

Equations

• AddOpposite.instMonoidWithZero = let __spread.0 := AddOpposite.instMonoid; let __spread.1 := AddOpposite.instMulZeroOneClass; MonoidWithZero.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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