Group structures on the multiplicative and additive opposites

Additive structures on αᵐᵒᵖ

@[instance_reducible]

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

Equations

• MulOpposite.instAddSemigroup = Function.Injective.addSemigroup MulOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup MulOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddRightCancelSemigroup = Function.Injective.addRightCancelSemigroup MulOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddCommMagma = Function.Injective.addCommMagma MulOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddCommSemigroup = Function.Injective.addCommSemigroup MulOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddZeroClass = Function.Injective.addZeroClass MulOpposite.unop ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddMonoid = Function.Injective.addMonoid MulOpposite.unop ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddCommMonoid = Function.Injective.addCommMonoid MulOpposite.unop ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instSubNegMonoid = Function.Injective.subNegMonoid MulOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddGroup = Function.Injective.addGroup MulOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• MulOpposite.instAddCommGroup = Function.Injective.addCommGroup MulOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 αᵃᵒᵖ

@[instance_reducible]

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

Equations

• MulOpposite.instSemigroup = { toMul := MulOpposite.instMul, mul_assoc := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddSemigroup = { toAdd := AddOpposite.instAdd, add_assoc := ⋯ }

@[instance_reducible]

instance MulOpposite.instLeftCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] : LeftCancelSemigroup αᵐᵒᵖ

Equations

• MulOpposite.instLeftCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, toIsLeftCancelMul := ⋯ }

@[instance_reducible]

instance AddOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] : AddLeftCancelSemigroup αᵃᵒᵖ

Equations

• AddOpposite.instAddLeftCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, toIsLeftCancelAdd := ⋯ }

@[instance_reducible]

instance MulOpposite.instRightCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] : RightCancelSemigroup αᵐᵒᵖ

Equations

• MulOpposite.instRightCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, toIsRightCancelMul := ⋯ }

@[instance_reducible]

instance AddOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] : AddRightCancelSemigroup αᵃᵒᵖ

Equations

• AddOpposite.instAddRightCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, toIsRightCancelAdd := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instCommSemigroup = { toSemigroup := MulOpposite.instSemigroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddCommSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, add_comm := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instMulOne = { toOne := MulOpposite.instOne, toMul := MulOpposite.instMul }

@[instance_reducible]

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

Equations

• AddOpposite.instAddZero = { toZero := AddOpposite.instZero, toAdd := AddOpposite.instAdd }

@[instance_reducible]

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

Equations

• MulOpposite.instMulOneClass = { toOne := MulOpposite.instOne, toMul := MulOpposite.instMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddZeroClass = { toZero := AddOpposite.instZero, toAdd := AddOpposite.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance MulOpposite.instLeftCancelMonoid {α : Type u_1} [RightCancelMonoid α] : LeftCancelMonoid αᵐᵒᵖ

Equations

• MulOpposite.instLeftCancelMonoid = { toMonoid := MulOpposite.instMonoid, toIsLeftCancelMul := ⋯ }

@[instance_reducible]

instance AddOpposite.instAddLeftCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] : AddLeftCancelMonoid αᵃᵒᵖ

Equations

• AddOpposite.instAddLeftCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, toIsLeftCancelAdd := ⋯ }

@[instance_reducible]

instance MulOpposite.instRightCancelMonoid {α : Type u_1} [LeftCancelMonoid α] : RightCancelMonoid αᵐᵒᵖ

Equations

• MulOpposite.instRightCancelMonoid = { toMonoid := MulOpposite.instMonoid, toIsRightCancelMul := ⋯ }

@[instance_reducible]

instance AddOpposite.instAddRightCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] : AddRightCancelMonoid αᵃᵒᵖ

Equations

• AddOpposite.instAddRightCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, toIsRightCancelAdd := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instCancelMonoid = { toLeftCancelMonoid := MulOpposite.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddCancelMonoid = { toAddLeftCancelMonoid := AddOpposite.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instCommMonoid = { toMonoid := MulOpposite.instMonoid, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddCommMonoid = { toAddMonoid := AddOpposite.instAddMonoid, add_comm := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instCancelCommMonoid = { toCommMonoid := MulOpposite.instCommMonoid, toIsLeftCancelMul := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddCancelCommMonoid = { toAddCommMonoid := AddOpposite.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• MulOpposite.instDivisionMonoid = { toDivInvMonoid := MulOpposite.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instSubtractionMonoid = { toSubNegMonoid := AddOpposite.instSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instDivisionCommMonoid = { toDivisionMonoid := MulOpposite.instDivisionMonoid, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instSubtractionCommMonoid = { toSubtractionMonoid := AddOpposite.instSubtractionMonoid, add_comm := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instGroup = { toDivInvMonoid := MulOpposite.instDivInvMonoid, inv_mul_cancel := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddGroup = { toSubNegMonoid := AddOpposite.instSubNegMonoid, neg_add_cancel := ⋯ }

@[instance_reducible]

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

Equations

• MulOpposite.instCommGroup = { toGroup := MulOpposite.instGroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• AddOpposite.instAddCommGroup = { toAddGroup := AddOpposite.instAddGroup, add_comm := ⋯ }

@[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

instance MulOpposite.instIsMulTorsionFree {α : Type u_1} [Monoid α] [IsMulTorsionFree α] : IsMulTorsionFree αᵐᵒᵖ

instance AddOpposite.instIsAddTorsionFree {α : Type u_1} [AddMonoid α] [IsAddTorsionFree α] : IsAddTorsionFree αᵃᵒᵖ

instance MulOpposite.instHasUniqueRoots {α : Type u_1} [Monoid α] [HasUniqueRoots α] : HasUniqueRoots αᵐᵒᵖ

instance AddOpposite.insthasUniqueDiv {α : Type u_1} [AddMonoid α] [HasUniqueDiv α] : HasUniqueDiv αᵃᵒᵖ

@[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 α

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

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

@[simp]

theorem MulOpposite.isMulCommutative_op_iff {α : Type u_1} [Mul α] : IsMulCommutative αᵐᵒᵖ ↔ IsMulCommutative α

@[simp]

theorem AddOpposite.isAddCommutative_op_iff {α : Type u_1} [Add α] : IsAddCommutative αᵃᵒᵖ ↔ IsAddCommutative α

instance MulOpposite.instIsMulCommutative {α : Type u_1} [Mul α] [IsMulCommutative α] : IsMulCommutative αᵐᵒᵖ

instance AddOpposite.instIsAddCommutative {α : Type u_1} [Add α] [IsAddCommutative α] : IsAddCommutative αᵃᵒᵖ

Multiplicative structures on αᵃᵒᵖ

@[instance_reducible]

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

Equations

• AddOpposite.instSemigroup = Function.Injective.semigroup AddOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instLeftCancelSemigroup = Function.Injective.leftCancelSemigroup AddOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instRightCancelSemigroup = Function.Injective.rightCancelSemigroup AddOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instCommSemigroup = Function.Injective.commSemigroup AddOpposite.unop ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instMulOneClass = Function.Injective.mulOneClass AddOpposite.unop ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.pow = { pow := fun (a : αᵃᵒᵖ) (b : β) => AddOpposite.op (AddOpposite.unop a ^ b) }

@[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

@[instance_reducible]

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

Equations

• AddOpposite.instMonoid = Function.Injective.monoid AddOpposite.unop ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instCommMonoid = Function.Injective.commMonoid AddOpposite.unop ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instDivInvMonoid = Function.Injective.divInvMonoid AddOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instGroup = Function.Injective.group AddOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• AddOpposite.instCommGroup = Function.Injective.commGroup AddOpposite.unop ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯