Documentation

@[implicit_reducible]

instance MulOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :

AddSemigroup αᵐᵒᵖ

AddLeftCancelSemigroup αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :

AddRightCancelSemigroup αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :

@[implicit_reducible]

instance MulOpposite.instAddCommMagma {α : Type u_1} [AddCommMagma α] :

AddCommMagma αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :

AddCommSemigroup αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :

AddZeroClass αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :

AddMonoid αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :

AddCommMonoid αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :

SubNegMonoid αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddGroup {α : Type u_1} [AddGroup α] :

AddGroup αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :

AddCommGroup αᵐᵒᵖ

Multiplicative structures on `αᵐᵒᵖ` #

We also generate additive structures on αᵃᵒᵖ using to_additive

instance MulOpposite.instIsRightCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :

IsRightCancelMul αᵐᵒᵖ

instance AddOpposite.instIsRightCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :

IsRightCancelAdd αᵃᵒᵖ

instance MulOpposite.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :

IsLeftCancelMul αᵐᵒᵖ

instance AddOpposite.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :

IsLeftCancelAdd αᵃᵒᵖ

instance MulOpposite.instIsCancelMul {α : Type u_1} [Mul α] [IsCancelMul α] :

IsCancelMul αᵐᵒᵖ

instance AddOpposite.instIsCancelAdd {α : Type u_1} [Add α] [IsCancelAdd α] :

IsCancelAdd αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instSemigroup {α : Type u_1} [Semigroup α] :

Semigroup αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :

AddSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instLeftCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :

LeftCancelSemigroup αᵐᵒᵖ

AddLeftCancelSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :

RightCancelSemigroup αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instRightCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :

AddRightCancelSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :

@[implicit_reducible]

instance MulOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :

CommSemigroup αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :

AddCommSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instMulOne {α : Type u_1} [MulOne α] :

MulOne αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddZero {α : Type u_1} [AddZero α] :

AddZero αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :

MulOneClass αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :

AddZeroClass αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instMonoid {α : Type u_1} [Monoid α] :

Monoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :

AddMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instLeftCancelMonoid {α : Type u_1} [RightCancelMonoid α] :

LeftCancelMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddLeftCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :

AddLeftCancelMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instRightCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :

RightCancelMonoid αᵐᵒᵖ

AddRightCancelMonoid αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddRightCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :

@[implicit_reducible]

instance MulOpposite.instCancelMonoid {α : Type u_1} [CancelMonoid α] :

CancelMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :

AddCancelMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :

CommMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :

AddCommMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :

CancelCommMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :

AddCancelCommMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :

DivInvMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :

SubNegMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :

DivisionMonoid αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :

SubtractionMonoid αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :

DivisionCommMonoid αᵐᵒᵖ

SubtractionCommMonoid αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instSubtractionCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :

@[implicit_reducible]

instance MulOpposite.instGroup {α : Type u_1} [Group α] :

Group αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddGroup {α : Type u_1} [AddGroup α] :

AddGroup αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instCommGroup {α : Type u_1} [CommGroup α] :

CommGroup αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :

AddCommGroup αᵃᵒᵖ

@[simp]

theorem MulOpposite.op_pow {α : Type u_1} [Monoid α] (x : α) (n : ℕ) :

op (x ^ n) = op x ^ n

@[simp]

theorem AddOpposite.op_nsmul {α : Type u_1} [AddMonoid α] (x : α) (n : ℕ) :

op (n • x) = n • op x

@[simp]

theorem MulOpposite.unop_pow {α : Type u_1} [Monoid α] (x : αᵐᵒᵖ) (n : ℕ) :

unop (x ^ n) = unop x ^ n

@[simp]

theorem AddOpposite.unop_nsmul {α : Type u_1} [AddMonoid α] (x : αᵃᵒᵖ) (n : ℕ) :

unop (n • x) = n • unop x

@[simp]

theorem MulOpposite.op_zpow {α : Type u_1} [DivInvMonoid α] (x : α) (z : ℤ) :

op (x ^ z) = op x ^ z

@[simp]

theorem AddOpposite.op_zsmul {α : Type u_1} [SubNegMonoid α] (x : α) (z : ℤ) :

op (z • x) = z • op x

@[simp]

theorem MulOpposite.unop_zpow {α : Type u_1} [DivInvMonoid α] (x : αᵐᵒᵖ) (z : ℤ) :

unop (x ^ z) = unop x ^ z

@[simp]

theorem AddOpposite.unop_zsmul {α : Type u_1} [SubNegMonoid α] (x : αᵃᵒᵖ) (z : ℤ) :

unop (z • x) = z • unop x

@[simp]

theorem MulOpposite.unop_div {α : Type u_1} [DivInvMonoid α] (x y : αᵐᵒᵖ) :

unop (x / y) = (unop y)⁻¹ * unop x

@[simp]

theorem AddOpposite.unop_sub {α : Type u_1} [SubNegMonoid α] (x y : αᵃᵒᵖ) :

unop (x - y) = -unop y + unop x

@[simp]

theorem MulOpposite.op_div {α : Type u_1} [DivInvMonoid α] (x y : α) :

op (x / y) = (op y)⁻¹ * op x

@[simp]

theorem AddOpposite.op_sub {α : Type u_1} [SubNegMonoid α] (x y : α) :

op (x - y) = -op y + op x

@[simp]

theorem MulOpposite.semiconjBy_op {α : Type u_1} [Mul α] {a x y : α} :

SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

@[simp]

theorem AddOpposite.addSemiconjBy_op {α : Type u_1} [Add α] {a x y : α} :

AddSemiconjBy (op a) (op y) (op x) ↔ AddSemiconjBy a x y

@[simp]

theorem MulOpposite.semiconjBy_unop {α : Type u_1} [Mul α] {a x y : αᵐᵒᵖ} :

SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

@[simp]

theorem AddOpposite.addSemiconjBy_unop {α : Type u_1} [Add α] {a x y : αᵃᵒᵖ} :

AddSemiconjBy (unop a) (unop y) (unop x) ↔ AddSemiconjBy a x y

theorem SemiconjBy.op {α : Type u_1} [Mul α] {a x y : α} (h : SemiconjBy a x y) :

SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x)

theorem AddSemiconjBy.op {α : Type u_1} [Add α] {a x y : α} (h : AddSemiconjBy a x y) :

AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x)

theorem SemiconjBy.unop {α : Type u_1} [Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) :

SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x)

theorem AddSemiconjBy.unop {α : Type u_1} [Add α] {a x y : αᵃᵒᵖ} (h : AddSemiconjBy a x y) :

AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x)

theorem Commute.op {α : Type u_1} [Mul α] {x y : α} (h : Commute x y) :

Commute (MulOpposite.op x) (MulOpposite.op y)

theorem AddCommute.op {α : Type u_1} [Add α] {x y : α} (h : AddCommute x y) :

AddCommute (AddOpposite.op x) (AddOpposite.op y)

theorem Commute.unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) :

Commute (MulOpposite.unop x) (MulOpposite.unop y)

theorem AddCommute.unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} (h : AddCommute x y) :

AddCommute (AddOpposite.unop x) (AddOpposite.unop y)

@[simp]

theorem MulOpposite.commute_op {α : Type u_1} [Mul α] {x y : α} :

Commute (op x) (op y) ↔ Commute x y

@[simp]

theorem AddOpposite.addCommute_op {α : Type u_1} [Add α] {x y : α} :

AddCommute (op x) (op y) ↔ AddCommute x y

@[simp]

theorem MulOpposite.commute_unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} :

Commute (unop x) (unop y) ↔ Commute x y

@[simp]

theorem AddOpposite.addCommute_unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} :

AddCommute (unop x) (unop y) ↔ AddCommute x y

theorem MulOpposite.isDedekindFiniteMonoid_iff {α : Type u_1} [MulOne α] :

IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

theorem AddOpposite.isDedekindFiniteAddMonoid_iff {α : Type u_1} [AddZero α] :

IsDedekindFiniteAddMonoid αᵃᵒᵖ ↔ IsDedekindFiniteAddMonoid α

IsDedekindFiniteMonoid αᵐᵒᵖ

instance MulOpposite.instIsDedekindFiniteMonoid {α : Type u_1} [MulOne α] [IsDedekindFiniteMonoid α] :

IsDedekindFiniteAddMonoid αᵃᵒᵖ

instance AddOpposite.instIsDedekindFiniteAddMonoid {α : Type u_1} [AddZero α] [IsDedekindFiniteAddMonoid α] :

Multiplicative structures on `αᵃᵒᵖ` #

@[implicit_reducible]

instance AddOpposite.instSemigroup {α : Type u_1} [Semigroup α] :

Semigroup αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :

LeftCancelSemigroup αᵃᵒᵖ

RightCancelSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :

@[implicit_reducible]

instance AddOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :

CommSemigroup αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :

MulOneClass αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.pow {α : Type u_1} {β : Type u_2} [Pow α β] :

Pow αᵃᵒᵖ β

@[simp]

theorem AddOpposite.op_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

op (a ^ b) = op a ^ b

@[simp]

theorem AddOpposite.unop_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵃᵒᵖ) (b : β) :

unop (a ^ b) = unop a ^ b

@[implicit_reducible]

instance AddOpposite.instMonoid {α : Type u_1} [Monoid α] :

Monoid αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :

CommMonoid αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :

DivInvMonoid αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instGroup {α : Type u_1} [Group α] :

Group αᵃᵒᵖ

@[implicit_reducible]

instance AddOpposite.instCommGroup {α : Type u_1} [CommGroup α] :

CommGroup αᵃᵒᵖ

instance AddOpposite.instMulTorsionFree {α : Type u_1} [Monoid α] [IsMulTorsionFree α] :

IsMulTorsionFree αᵐᵒᵖ