Group structures on the multiplicative and additive opposites #

Additive structures on `αᵐᵒᵖ` #

source

instance MulOpposite.instNatCast {α : Type u_1} [NatCast α] :

NatCast αᵐᵒᵖ

Equations

MulOpposite.instNatCast = { natCast := fun (n : ℕ) => MulOpposite.op ↑n }

source

instance AddOpposite.instNatCast {α : Type u_1} [NatCast α] :

NatCast αᵃᵒᵖ

Equations

AddOpposite.instNatCast = { natCast := fun (n : ℕ) => AddOpposite.op ↑n }

source

instance MulOpposite.instIntCast {α : Type u_1} [IntCast α] :

IntCast αᵐᵒᵖ

Equations

MulOpposite.instIntCast = { intCast := fun (n : ℤ) => MulOpposite.op ↑n }

source

instance AddOpposite.instIntCast {α : Type u_1} [IntCast α] :

IntCast αᵃᵒᵖ

Equations

AddOpposite.instIntCast = { intCast := fun (n : ℤ) => AddOpposite.op ↑n }

source

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

AddSemigroup αᵐᵒᵖ

Equations

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

source

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

AddLeftCancelSemigroup αᵐᵒᵖ

Equations

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

source

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

AddRightCancelSemigroup αᵐᵒᵖ

Equations

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

source

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

AddCommSemigroup αᵐᵒᵖ

Equations

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

source

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

AddZeroClass αᵐᵒᵖ

Equations

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

source

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

AddMonoid αᵐᵒᵖ

Equations

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

source

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

AddCommMonoid αᵐᵒᵖ

Equations

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

source

instance MulOpposite.instAddMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] :

AddMonoidWithOne αᵐᵒᵖ

Equations

MulOpposite.instAddMonoidWithOne = { toNatCast := MulOpposite.instNatCast, toAddMonoid := MulOpposite.instAddMonoid, toOne := MulOpposite.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

source

instance MulOpposite.instAddCommMonoidWithOne {α : Type u_1} [AddCommMonoidWithOne α] :

AddCommMonoidWithOne αᵐᵒᵖ

Equations

MulOpposite.instAddCommMonoidWithOne = { toAddMonoidWithOne := MulOpposite.instAddMonoidWithOne, add_comm := ⋯ }

source

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

SubNegMonoid αᵐᵒᵖ

Equations

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

source

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

AddGroup αᵐᵒᵖ

Equations

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

source

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

AddCommGroup αᵐᵒᵖ

Equations

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

source

instance MulOpposite.instAddGroupWithOne {α : Type u_1} [AddGroupWithOne α] :

AddGroupWithOne αᵐᵒᵖ

Equations

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

source

instance MulOpposite.instAddCommGroupWithOne {α : Type u_1} [AddCommGroupWithOne α] :

AddCommGroupWithOne αᵐᵒᵖ

Equations

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

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.instIsAddRightCancel {α : Type u_1} [Add α] [IsLeftCancelAdd α] :

IsRightCancelAdd αᵃᵒᵖ

source

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

IsLeftCancelMul αᵐᵒᵖ

source

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

IsLeftCancelAdd αᵃᵒᵖ

source

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

Semigroup αᵐᵒᵖ

Equations

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

source

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

AddSemigroup αᵃᵒᵖ

Equations

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

source

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

LeftCancelSemigroup αᵐᵒᵖ

Equations

MulOpposite.instLeftCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, mul_left_cancel := ⋯ }

source

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

AddLeftCancelSemigroup αᵃᵒᵖ

Equations

AddOpposite.instAddLeftCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, add_left_cancel := ⋯ }

source

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

RightCancelSemigroup αᵐᵒᵖ

Equations

MulOpposite.instRightCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, mul_right_cancel := ⋯ }

source

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

AddRightCancelSemigroup αᵃᵒᵖ

Equations

AddOpposite.instAddRightCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, add_right_cancel := ⋯ }

source

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

CommSemigroup αᵐᵒᵖ

Equations

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

source

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

AddCommSemigroup αᵃᵒᵖ

Equations

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

source

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

MulOneClass αᵐᵒᵖ

Equations

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

source

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

AddZeroClass αᵃᵒᵖ

Equations

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

source

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

Monoid αᵐᵒᵖ

Equations

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

source

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

AddMonoid αᵃᵒᵖ

Equations

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

source

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

LeftCancelMonoid αᵐᵒᵖ

Equations

MulOpposite.instLeftCancelMonoid = { toMonoid := MulOpposite.instMonoid, mul_left_cancel := ⋯ }

source

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

AddLeftCancelMonoid αᵃᵒᵖ

Equations

AddOpposite.instAddLeftCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, add_left_cancel := ⋯ }

source

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

RightCancelMonoid αᵐᵒᵖ

Equations

MulOpposite.instRightCancelMonoid = { toMonoid := MulOpposite.instMonoid, mul_right_cancel := ⋯ }

source

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

AddRightCancelMonoid αᵃᵒᵖ

Equations

AddOpposite.instAddRightCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, add_right_cancel := ⋯ }

source

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

CancelMonoid αᵐᵒᵖ

Equations

MulOpposite.instCancelMonoid = { toLeftCancelMonoid := MulOpposite.instLeftCancelMonoid, mul_right_cancel := ⋯ }

source

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

AddCancelMonoid αᵃᵒᵖ

Equations

AddOpposite.instAddCancelMonoid = { toAddLeftCancelMonoid := AddOpposite.instAddLeftCancelMonoid, add_right_cancel := ⋯ }

source

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

CommMonoid αᵐᵒᵖ

Equations

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

source

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

AddCommMonoid αᵃᵒᵖ

Equations

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

source

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

CancelCommMonoid αᵐᵒᵖ

Equations

MulOpposite.instCancelCommMonoid = { toCommMonoid := MulOpposite.instCommMonoid, mul_left_cancel := ⋯ }

source

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

AddCancelCommMonoid αᵃᵒᵖ

Equations

AddOpposite.instAddCancelCommMonoid = { toAddCommMonoid := AddOpposite.instAddCommMonoid, add_left_cancel := ⋯ }

source

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

DivInvMonoid αᵐᵒᵖ

Equations

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

source

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

SubNegMonoid αᵃᵒᵖ

Equations

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

source

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

DivisionMonoid αᵐᵒᵖ

Equations

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

source

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

SubtractionMonoid αᵃᵒᵖ

Equations

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

source

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

DivisionCommMonoid αᵐᵒᵖ

Equations

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

source

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

SubtractionCommMonoid αᵃᵒᵖ

Equations

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

source

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

Group αᵐᵒᵖ

Equations

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

source

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

AddGroup αᵃᵒᵖ

Equations

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

source

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

CommGroup αᵐᵒᵖ

Equations

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

source

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

AddCommGroup αᵃᵒᵖ

Equations

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

source

@[simp]

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

op (x ^ n) = op x ^ n

source

@[simp]

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

unop (x ^ n) = unop x ^ n

source

@[simp]

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

op (x ^ z) = op x ^ z

source

@[simp]

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

unop (x ^ z) = unop x ^ z

source

@[simp]

theorem MulOpposite.op_natCast {α : Type u_1} [NatCast α] (n : ℕ) :

op ↑n = ↑n

source

@[simp]

theorem AddOpposite.op_natCast {α : Type u_1} [NatCast α] (n : ℕ) :

op ↑n = ↑n

source

@[simp]

theorem MulOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :

op (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem AddOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :

op (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem MulOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ℤ) :

op ↑n = ↑n

source

@[simp]

theorem AddOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ℤ) :

op ↑n = ↑n

source

@[simp]

theorem MulOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ℕ) :

unop ↑n = ↑n

source

@[simp]

theorem AddOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ℕ) :

unop ↑n = ↑n

source

@[simp]

theorem MulOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :

unop (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem AddOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :

unop (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem MulOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ℤ) :

unop ↑n = ↑n

source

@[simp]

theorem AddOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ℤ) :

unop ↑n = ↑n

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

Multiplicative structures on `αᵃᵒᵖ` #

source

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

Semigroup αᵃᵒᵖ

Equations

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

source

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

LeftCancelSemigroup αᵃᵒᵖ

Equations

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

source

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

RightCancelSemigroup αᵃᵒᵖ

Equations

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

source

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

CommSemigroup αᵃᵒᵖ

Equations

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

source

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

MulOneClass αᵃᵒᵖ

Equations

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

source

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

Pow αᵃᵒᵖ β

Equations

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

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 AddOpposite.instMonoid {α : Type u_1} [Monoid α] :

Monoid αᵃᵒᵖ

Equations

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

source

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

CommMonoid αᵃᵒᵖ

Equations

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

source

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

DivInvMonoid αᵃᵒᵖ

Equations

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

source

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

Group αᵃᵒᵖ

Equations

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

source

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

CommGroup αᵃᵒᵖ

Equations

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

source

instance AddOpposite.instAddCommMonoidWithOne {α : Type u_1} [AddCommMonoidWithOne α] :

AddCommMonoidWithOne αᵃᵒᵖ

Equations

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

source

instance AddOpposite.instAddCommGroupWithOne {α : Type u_1} [AddCommGroupWithOne α] :

AddCommGroupWithOne αᵃᵒᵖ

Equations

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

Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

Multiplicative structures on αᵐᵒᵖ #

Multiplicative structures on αᵃᵒᵖ #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #