Documentation

Mathlib.Algebra.GroupWithZero.Opposite

Opposites of groups with zero #

source
@[implicit_reducible]
instance MulOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass αᵐᵒᵖ
source
@[implicit_reducible]
instance MulOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
MulZeroOneClass αᵐᵒᵖ
source
@[implicit_reducible]
instance MulOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
SemigroupWithZero αᵐᵒᵖ
source
@[implicit_reducible]
instance MulOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
MonoidWithZero αᵐᵒᵖ
source
@[implicit_reducible]
instance MulOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
GroupWithZero αᵐᵒᵖ
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
@[implicit_reducible]
instance AddOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass αᵃᵒᵖ
source
@[implicit_reducible]
instance AddOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
MulZeroOneClass αᵃᵒᵖ
source
@[implicit_reducible]
instance AddOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
SemigroupWithZero αᵃᵒᵖ
source
@[implicit_reducible]
instance AddOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
MonoidWithZero αᵃᵒᵖ
source
instance AddOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] :
NoZeroDivisors αᵃᵒᵖ
source
@[implicit_reducible]
instance AddOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
GroupWithZero αᵃᵒᵖ