Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

source
@[instance_reducible]
instance MulOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
AddRightCancelSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommMagma {α : Type u_1} [AddCommMagma α] :
AddCommMagma αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
AddCommSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
AddZeroClass αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :
AddMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
AddCommMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :
SubNegMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddGroup {α : Type u_1} [AddGroup α] :
AddGroup αᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
AddCommGroup αᵐᵒᵖ

Multiplicative structures on αᵐᵒᵖ #

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

source
instance MulOpposite.instIsRightCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :
IsRightCancelMul αᵐᵒᵖ
source
instance AddOpposite.instIsRightCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
IsRightCancelAdd αᵃᵒᵖ
source
instance MulOpposite.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :
IsLeftCancelMul αᵐᵒᵖ
source
instance AddOpposite.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :
IsLeftCancelAdd αᵃᵒᵖ
source
instance MulOpposite.instIsCancelMul {α : Type u_1} [Mul α] [IsCancelMul α] :
IsCancelMul αᵐᵒᵖ
source
instance AddOpposite.instIsCancelAdd {α : Type u_1} [Add α] [IsCancelAdd α] :
IsCancelAdd αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instSemigroup {α : Type u_1} [Semigroup α] :
Semigroup αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instLeftCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
LeftCancelSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
AddLeftCancelSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instRightCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
RightCancelSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
AddRightCancelSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
CommSemigroup αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
AddCommSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instMulOne {α : Type u_1} [MulOne α] :
MulOne αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddZero {α : Type u_1} [AddZero α] :
AddZero αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :
MulOneClass αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
AddZeroClass αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instMonoid {α : Type u_1} [Monoid α] :
Monoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :
AddMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instLeftCancelMonoid {α : Type u_1} [RightCancelMonoid α] :
LeftCancelMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddLeftCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :
AddLeftCancelMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instRightCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :
RightCancelMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddRightCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :
AddRightCancelMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCancelMonoid {α : Type u_1} [CancelMonoid α] :
CancelMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :
AddCancelMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :
CommMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
AddCommMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :
CancelCommMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :
AddCancelCommMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
DivInvMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :
SubNegMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :
DivisionMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :
SubtractionMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :
DivisionCommMonoid αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instSubtractionCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :
SubtractionCommMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instGroup {α : Type u_1} [Group α] :
Group αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddGroup {α : Type u_1} [AddGroup α] :
AddGroup αᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCommGroup {α : Type u_1} [CommGroup α] :
CommGroup αᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
AddCommGroup αᵃᵒᵖ
source
@[simp]
theorem MulOpposite.op_pow {α : Type u_1} [Monoid α] (x : α) (n : ℕ) :
op (x ^ n) = op x ^ n
source
@[simp]
theorem AddOpposite.op_nsmul {α : Type u_1} [AddMonoid α] (x : α) (n : ℕ) :
op (n • x) = n • op x
source
@[simp]
theorem MulOpposite.unop_pow {α : Type u_1} [Monoid α] (x : αᵐᵒᵖ) (n : ℕ) :
unop (x ^ n) = unop x ^ n
source
@[simp]
theorem AddOpposite.unop_nsmul {α : Type u_1} [AddMonoid α] (x : αᵃᵒᵖ) (n : ℕ) :
unop (n • x) = n • unop x
source
instance MulOpposite.instIsMulTorsionFree {α : Type u_1} [Monoid α] [IsMulTorsionFree α] :
IsMulTorsionFree αᵐᵒᵖ
source
instance AddOpposite.instIsAddTorsionFree {α : Type u_1} [AddMonoid α] [IsAddTorsionFree α] :
IsAddTorsionFree αᵃᵒᵖ
source
instance MulOpposite.instHasUniqueRoots {α : Type u_1} [Monoid α] [HasUniqueRoots α] :
HasUniqueRoots αᵐᵒᵖ
source
instance AddOpposite.insthasUniqueDiv {α : Type u_1} [AddMonoid α] [HasUniqueDiv α] :
HasUniqueDiv αᵃᵒᵖ
source
@[simp]
theorem MulOpposite.op_zpow {α : Type u_1} [DivInvMonoid α] (x : α) (z : ℤ) :
op (x ^ z) = op x ^ z
source
@[simp]
theorem AddOpposite.op_zsmul {α : Type u_1} [SubNegMonoid α] (x : α) (z : ℤ) :
op (z • x) = z • op x
source
@[simp]
theorem MulOpposite.unop_zpow {α : Type u_1} [DivInvMonoid α] (x : αᵐᵒᵖ) (z : ℤ) :
unop (x ^ z) = unop x ^ z
source
@[simp]
theorem AddOpposite.unop_zsmul {α : Type u_1} [SubNegMonoid α] (x : αᵃᵒᵖ) (z : ℤ) :
unop (z • x) = z • unop x
source
@[simp]
theorem MulOpposite.unop_div {α : Type u_1} [DivInvMonoid α] (x y : αᵐᵒᵖ) :
unop (x / y) = (unop y)⁻¹ * unop x
source
@[simp]
theorem AddOpposite.unop_sub {α : Type u_1} [SubNegMonoid α] (x y : αᵃᵒᵖ) :
unop (x - y) = -unop y + unop x
source
@[simp]
theorem MulOpposite.op_div {α : Type u_1} [DivInvMonoid α] (x y : α) :
op (x / y) = (op y)⁻¹ * op x
source
@[simp]
theorem AddOpposite.op_sub {α : Type u_1} [SubNegMonoid α] (x y : α) :
op (x - y) = -op y + op x
source
@[simp]
theorem MulOpposite.semiconjBy_op {α : Type u_1} [Mul α] {a x y : α} :
SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y
source
@[simp]
theorem AddOpposite.addSemiconjBy_op {α : Type u_1} [Add α] {a x y : α} :
AddSemiconjBy (op a) (op y) (op x) ↔ AddSemiconjBy a x y
source
@[simp]
theorem MulOpposite.semiconjBy_unop {α : Type u_1} [Mul α] {a x y : αᵐᵒᵖ} :
SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
source
@[simp]
theorem AddOpposite.addSemiconjBy_unop {α : Type u_1} [Add α] {a x y : αᵃᵒᵖ} :
AddSemiconjBy (unop a) (unop y) (unop x) ↔ AddSemiconjBy a x y
source
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)
source
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)
source
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)
source
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)
source
theorem Commute.op {α : Type u_1} [Mul α] {x y : α} (h : Commute x y) :
Commute (MulOpposite.op x) (MulOpposite.op y)
source
theorem AddCommute.op {α : Type u_1} [Add α] {x y : α} (h : AddCommute x y) :
AddCommute (AddOpposite.op x) (AddOpposite.op y)
source
theorem Commute.unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) :
Commute (MulOpposite.unop x) (MulOpposite.unop y)
source
theorem AddCommute.unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} (h : AddCommute x y) :
AddCommute (AddOpposite.unop x) (AddOpposite.unop y)
source
@[simp]
theorem MulOpposite.commute_op {α : Type u_1} [Mul α] {x y : α} :
Commute (op x) (op y) ↔ Commute x y
source
@[simp]
theorem AddOpposite.addCommute_op {α : Type u_1} [Add α] {x y : α} :
AddCommute (op x) (op y) ↔ AddCommute x y
source
@[simp]
theorem MulOpposite.commute_unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} :
Commute (unop x) (unop y) ↔ Commute x y
source
@[simp]
theorem AddOpposite.addCommute_unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} :
AddCommute (unop x) (unop y) ↔ AddCommute x y
source
theorem MulOpposite.isDedekindFiniteMonoid_iff {α : Type u_1} [MulOne α] :
IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α
source
theorem AddOpposite.isDedekindFiniteAddMonoid_iff {α : Type u_1} [AddZero α] :
IsDedekindFiniteAddMonoid αᵃᵒᵖ ↔ IsDedekindFiniteAddMonoid α
source
instance MulOpposite.instIsDedekindFiniteMonoid {α : Type u_1} [MulOne α] [IsDedekindFiniteMonoid α] :
IsDedekindFiniteMonoid αᵐᵒᵖ
source
instance AddOpposite.instIsDedekindFiniteAddMonoid {α : Type u_1} [AddZero α] [IsDedekindFiniteAddMonoid α] :
IsDedekindFiniteAddMonoid αᵃᵒᵖ
source
@[simp]
theorem MulOpposite.isMulCommutative_op_iff {α : Type u_1} [Mul α] :
IsMulCommutative αᵐᵒᵖ ↔ IsMulCommutative α
source
@[simp]
theorem AddOpposite.isAddCommutative_op_iff {α : Type u_1} [Add α] :
IsAddCommutative αᵃᵒᵖ ↔ IsAddCommutative α
source
instance MulOpposite.instIsMulCommutative {α : Type u_1} [Mul α] [IsMulCommutative α] :
IsMulCommutative αᵐᵒᵖ
source
instance AddOpposite.instIsAddCommutative {α : Type u_1} [Add α] [IsAddCommutative α] :
IsAddCommutative αᵃᵒᵖ

Multiplicative structures on αᵃᵒᵖ #

source
@[instance_reducible]
instance AddOpposite.instSemigroup {α : Type u_1} [Semigroup α] :
Semigroup αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
LeftCancelSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
RightCancelSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
CommSemigroup αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :
MulOneClass αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.pow {α : Type u_1} {β : Type u_2} [Pow α β] :
Pow αᵃᵒᵖ β
source
@[simp]
theorem AddOpposite.op_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
op (a ^ b) = op a ^ b
source
@[simp]
theorem AddOpposite.unop_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵃᵒᵖ) (b : β) :
unop (a ^ b) = unop a ^ b
source
@[instance_reducible]
instance AddOpposite.instMonoid {α : Type u_1} [Monoid α] :
Monoid αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :
CommMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
DivInvMonoid αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instGroup {α : Type u_1} [Group α] :
Group αᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instCommGroup {α : Type u_1} [CommGroup α] :
CommGroup αᵃᵒᵖ