Group structures on the multiplicative and additive opposites

Additive structures on αᵐᵒᵖ

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MulOpposite.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

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

Equations

• MulOpposite.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MulOpposite.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• MulOpposite.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

Multiplicative structures on αᵐᵒᵖ

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

instance AddOpposite.instIsAddRightCancel {α : Type u_1} [Add α] [IsLeftCancelAdd α] : IsRightCancelAdd αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.instIsRightCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] : IsRightCancelMul αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance AddOpposite.instIsAddLeftCancel {α : Type u_1} [Add α] [IsRightCancelAdd α] : IsLeftCancelAdd αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] : IsLeftCancelMul αᵐᵒᵖ

Equations

• ⋯ = ⋯

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

Equations

• AddOpposite.instAddSemigroup = AddSemigroup.mk ⋯

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

Equations

• MulOpposite.instSemigroup = Semigroup.mk ⋯

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

Equations

• AddOpposite.instAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

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

Equations

• MulOpposite.instLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯

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

Equations

• AddOpposite.instAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

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

Equations

• MulOpposite.instRightCancelSemigroup = RightCancelSemigroup.mk ⋯

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

Equations

• AddOpposite.instAddCommSemigroup = AddCommSemigroup.mk ⋯

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

Equations

• MulOpposite.instCommSemigroup = CommSemigroup.mk ⋯

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

Equations

• AddOpposite.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

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

Equations

• MulOpposite.instMulOneClass = MulOneClass.mk ⋯ ⋯

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

Equations

• AddOpposite.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) ⋯ ⋯

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

Equations

• MulOpposite.instMonoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop a ^ n)) ⋯ ⋯

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

Equations

• AddOpposite.instAddLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯

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

Equations

• MulOpposite.instLeftCancelMonoid = LeftCancelMonoid.mk ⋯

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

Equations

• AddOpposite.instAddRightCancelMonoid = AddRightCancelMonoid.mk ⋯

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

Equations

• MulOpposite.instRightCancelMonoid = RightCancelMonoid.mk ⋯

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

Equations

• AddOpposite.instAddCancelMonoid = AddCancelMonoid.mk ⋯

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

Equations

• MulOpposite.instCancelMonoid = CancelMonoid.mk ⋯

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

Equations

• AddOpposite.instAddCommMonoid = AddCommMonoid.mk ⋯

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

Equations

• MulOpposite.instCommMonoid = CommMonoid.mk ⋯

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

Equations

• AddOpposite.instAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯

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

Equations

• MulOpposite.instCancelCommMonoid = CancelCommMonoid.mk ⋯

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

Equations

• AddOpposite.instSubNegMonoid = SubNegMonoid.mk ⋯ (fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) ⋯ ⋯ ⋯

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

Equations

• MulOpposite.instDivInvMonoid = DivInvMonoid.mk ⋯ (fun (n : ℤ) (a : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop a ^ n)) ⋯ ⋯ ⋯

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

Equations

• AddOpposite.instSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• MulOpposite.instDivisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• AddOpposite.instSubtractionCommMonoid = SubtractionCommMonoid.mk ⋯

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

Equations

• MulOpposite.instDivisionCommMonoid = DivisionCommMonoid.mk ⋯

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

Equations

• AddOpposite.instAddGroup = AddGroup.mk ⋯

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

Equations

• MulOpposite.instGroup = Group.mk ⋯

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

Equations

• AddOpposite.instAddCommGroup = AddCommGroup.mk ⋯

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

Equations

• MulOpposite.instCommGroup = CommGroup.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulOpposite.unop_div {α : Type u_1} [DivInvMonoid α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : MulOpposite.unop (x / y) = (MulOpposite.unop y)⁻¹ * MulOpposite.unop x

@[simp]

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

@[simp]

theorem MulOpposite.op_div {α : Type u_1} [DivInvMonoid α] (x : α) (y : α) : MulOpposite.op (x / y) = (MulOpposite.op y)⁻¹ * MulOpposite.op x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.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.unop {α : Type u_1} [Add α] {a : αᵃᵒᵖ} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} (h : AddSemiconjBy a x y) : AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop 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 AddCommute.op {α : Type u_1} [Add α] {x : α} {y : α} (h : AddCommute x y) : AddCommute (AddOpposite.op x) (AddOpposite.op y)

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulOpposite.opAddEquiv_symm_apply {α : Type u_1} [Add α] : ⇑MulOpposite.opAddEquiv.symm = MulOpposite.unop

@[simp]

theorem MulOpposite.opAddEquiv_apply {α : Type u_1} [Add α] : ⇑MulOpposite.opAddEquiv = MulOpposite.op

def MulOpposite.opAddEquiv {α : Type u_1} [Add α] : α ≃+ αᵐᵒᵖ

The function MulOpposite.op is an additive equivalence.

Equations

• MulOpposite.opAddEquiv = { toEquiv := MulOpposite.opEquiv, map_add' := ⋯ }

@[simp]

theorem MulOpposite.opAddEquiv_toEquiv {α : Type u_1} [Add α] : ↑MulOpposite.opAddEquiv = MulOpposite.opEquiv

Multiplicative structures on αᵃᵒᵖ

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 : β) : AddOpposite.op (a ^ b) = AddOpposite.op a ^ b

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• AddOpposite.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

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

Equations

• AddOpposite.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem AddOpposite.opMulEquiv_apply {α : Type u_1} [Mul α] : ⇑AddOpposite.opMulEquiv = AddOpposite.op

@[simp]

theorem AddOpposite.opMulEquiv_symm_apply {α : Type u_1} [Mul α] : ⇑AddOpposite.opMulEquiv.symm = AddOpposite.unop

def AddOpposite.opMulEquiv {α : Type u_1} [Mul α] : α ≃* αᵃᵒᵖ

The function AddOpposite.op is a multiplicative equivalence.

Equations

• AddOpposite.opMulEquiv = { toEquiv := AddOpposite.opEquiv, map_mul' := ⋯ }

@[simp]

theorem AddOpposite.opMulEquiv_toEquiv {α : Type u_1} [Mul α] : ↑AddOpposite.opMulEquiv = AddOpposite.opEquiv

def AddEquiv.neg' (G : Type u_2) [SubtractionMonoid G] : G ≃+ Gᵃᵒᵖ

Negation on an additive group is an AddEquiv to the opposite group. When G is commutative, there is AddEquiv.inv.

Equations

• AddEquiv.neg' G = { toEquiv := Equiv.trans (Equiv.neg G) AddOpposite.opEquiv, map_add' := ⋯ }

@[simp]

theorem AddEquiv.neg'_apply (G : Type u_2) [SubtractionMonoid G] : ⇑(AddEquiv.neg' G) = AddOpposite.op ∘ Neg.neg

@[simp]

theorem AddEquiv.neg'_symm_apply (G : Type u_2) [SubtractionMonoid G] : ⇑(AddEquiv.neg' G).symm = Neg.neg ∘ AddOpposite.unop

@[simp]

theorem MulEquiv.inv'_symm_apply (G : Type u_2) [DivisionMonoid G] : ⇑(MulEquiv.inv' G).symm = Inv.inv ∘ MulOpposite.unop

@[simp]

theorem MulEquiv.inv'_apply (G : Type u_2) [DivisionMonoid G] : ⇑(MulEquiv.inv' G) = MulOpposite.op ∘ Inv.inv

def MulEquiv.inv' (G : Type u_2) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ

Inversion on a group is a MulEquiv to the opposite group. When G is commutative, there is MulEquiv.inv.

Equations

• MulEquiv.inv' G = { toEquiv := Equiv.trans (Equiv.inv G) MulOpposite.opEquiv, map_mul' := ⋯ }

def AddHom.toOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : AddHom M Nᵃᵒᵖ

An additive semigroup homomorphism f : AddHom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism to Sᵃᵒᵖ.

Equations

• f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_add' := ⋯ }

@[simp]

theorem MulHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

@[simp]

theorem AddHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

def MulHom.toOpposite {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ

A semigroup homomorphism f : M →ₙ* N such that f x commutes with f y for all x, y defines a semigroup homomorphism to Nᵐᵒᵖ.

Equations

• f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯ }

def AddHom.fromOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : AddHom Mᵃᵒᵖ N

An additive semigroup homomorphism f : AddHom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism from Mᵃᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }

@[simp]

theorem AddHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

@[simp]

theorem MulHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

def MulHom.fromOpposite {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : Mᵐᵒᵖ →ₙ* N

A semigroup homomorphism f : M →ₙ* N such that f x commutes with f y for all x, y defines a semigroup homomorphism from Mᵐᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯ }

def AddMonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : M →+ Nᵃᵒᵖ

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism to Sᵃᵒᵖ.

Equations

• f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

@[simp]

theorem MonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

def MonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : M →* Nᵐᵒᵖ

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism to Nᵐᵒᵖ.

Equations

• f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : Mᵃᵒᵖ →+ N

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism from Mᵃᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

@[simp]

theorem AddMonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

def MonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) : Mᵐᵒᵖ →* N

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism from Mᵐᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯ }

def AddUnits.opEquiv {M : Type u_2} [AddMonoid M] : AddUnits Mᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ

The additive units of the additive opposites are equivalent to the additive opposites of the additive units.

Equations

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

def Units.opEquiv {M : Type u_2} [Monoid M] : Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ

The units of the opposites are equivalent to the opposites of the units.

Equations

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

@[simp]

theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) : ↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u

@[simp]

theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : Mᵐᵒᵖˣ) : ↑(MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop ↑u

@[simp]

theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) : ↑(AddUnits.opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)

@[simp]

theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mˣᵐᵒᵖ) : ↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)

theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) : IsAddUnit (AddOpposite.op m)

theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) : IsUnit (MulOpposite.op m)

theorem IsAddUnit.unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} (h : IsAddUnit m) : IsAddUnit (AddOpposite.unop m)

theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) : IsUnit (MulOpposite.unop m)

@[simp]

theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} : IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m

@[simp]

theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} : IsUnit (MulOpposite.op m) ↔ IsUnit m

@[simp]

theorem isAddUnit_unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} : IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m

@[simp]

theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} : IsUnit (MulOpposite.unop m) ↔ IsUnit m

def AddHom.op {M : Type u_2} {N : Type u_3} [Add M] [Add N] : AddHom M N ≃ AddHom Mᵃᵒᵖ Nᵃᵒᵖ

An additive semigroup homomorphism AddHom M N can equivalently be viewed as an additive semigroup homomorphism AddHom Mᵃᵒᵖ Nᵃᵒᵖ. This is the action of the (fully faithful)ᵃᵒᵖ-functor on morphisms.

Equations

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

@[simp]

theorem AddHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) : ∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

@[simp]

theorem MulHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) : ∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

@[simp]

theorem MulHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) : ∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

@[simp]

theorem AddHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) : ∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

def MulHom.op {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ)

A semigroup homomorphism M →ₙ* N can equivalently be viewed as a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def AddHom.unop {M : Type u_2} {N : Type u_3} [Add M] [Add N] : AddHom Mᵃᵒᵖ Nᵃᵒᵖ ≃ AddHom M N

The 'unopposite' of an additive semigroup homomorphism Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ. Inverse to AddHom.op.

Equations

• AddHom.unop = AddHom.op.symm

def MulHom.unop {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] : (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)

The 'unopposite' of a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. Inverse to MulHom.op.

Equations

• MulHom.unop = MulHom.op.symm

@[simp]

theorem AddHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) : ∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

@[simp]

theorem AddHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) : ∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

def AddHom.mulOp {M : Type u_2} {N : Type u_3} [Add M] [Add N] : AddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ

An additive semigroup homomorphism AddHom M N can equivalently be viewed as an additive homomorphism AddHom Mᵐᵒᵖ Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def AddHom.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] : AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β

The 'unopposite' of an additive semigroup hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to AddHom.mul_op.

Equations

• AddHom.mulUnop = AddHom.mulOp.symm

def AddMonoidHom.op {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵃᵒᵖ →+ Nᵃᵒᵖ)

An additive monoid homomorphism M →+ N can equivalently be viewed as an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. This is the action of the (fully faithful) ᵃᵒᵖ-functor on morphisms.

Equations

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

@[simp]

theorem AddMonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) : ∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

@[simp]

theorem MonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) : ∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

@[simp]

theorem AddMonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : ∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

@[simp]

theorem MonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) : ∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

def MonoidHom.op {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ)

A monoid homomorphism M →* N can equivalently be viewed as a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def AddMonoidHom.unop {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] : (Mᵃᵒᵖ →+ Nᵃᵒᵖ) ≃ (M →+ N)

The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. Inverse to AddMonoidHom.op.

Equations

• AddMonoidHom.unop = AddMonoidHom.op.symm

def MonoidHom.unop {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)

The 'unopposite' of a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. Inverse to MonoidHom.op.

Equations

• MonoidHom.unop = MonoidHom.op.symm

def AddEquiv.opOp (M : Type u_2) [Add M] : M ≃+ Mᵃᵒᵖᵃᵒᵖ

A additive monoid is isomorphic to the opposite of its opposite.

Equations

• AddEquiv.opOp M = { toEquiv := AddOpposite.opEquiv.trans AddOpposite.opEquiv, map_add' := ⋯ }

@[simp]

theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] : ∀ (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op a)

@[simp]

theorem MulEquiv.opOp_symm_apply (M : Type u_2) [Mul M] : ∀ (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.opOp M).symm a = MulOpposite.unop (MulOpposite.unop a)

@[simp]

theorem AddEquiv.opOp_apply (M : Type u_2) [Add M] : ∀ (a : M), (AddEquiv.opOp M) a = AddOpposite.op (AddOpposite.op a)

@[simp]

theorem AddEquiv.opOp_symm_apply (M : Type u_2) [Add M] : ∀ (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.opOp M).symm a = AddOpposite.unop (AddOpposite.unop a)

def MulEquiv.opOp (M : Type u_2) [Mul M] : M ≃* Mᵐᵒᵖᵐᵒᵖ

A monoid is isomorphic to the opposite of its opposite.

Equations

• MulEquiv.opOp M = { toEquiv := MulOpposite.opEquiv.trans MulOpposite.opEquiv, map_mul' := ⋯ }

@[simp]

theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) : ∀ (a : M), (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

@[simp]

theorem AddMonoidHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : ∀ (a : Mᵐᵒᵖ), (AddMonoidHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

def AddMonoidHom.mulOp {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ)

An additive homomorphism M →+ N can equivalently be viewed as an additive homomorphism Mᵐᵒᵖ →+ Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def AddMonoidHom.mulUnop {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] : (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)

The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to AddMonoidHom.mul_op.

Equations

• AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm

@[simp]

theorem AddEquiv.mulOp_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)

@[simp]

theorem AddEquiv.mulOp_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) : AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)

def AddEquiv.mulOp {α : Type u_2} {β : Type u_3} [Add α] [Add β] : α ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ)

An iso α ≃+ β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.

Equations

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

def AddEquiv.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] : αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)

The 'unopposite' of an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ. Inverse to AddEquiv.mul_op.

Equations

• AddEquiv.mulUnop = AddEquiv.mulOp.symm

def AddEquiv.op {α : Type u_2} {β : Type u_3} [Add α] [Add β] : α ≃+ β ≃ (αᵃᵒᵖ ≃+ βᵃᵒᵖ)

An iso α ≃+ β can equivalently be viewed as an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ.

Equations

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

@[simp]

theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) : ∀ (a : β), (MulEquiv.op.symm f).symm a = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a

@[simp]

theorem AddEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : ∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

@[simp]

theorem MulEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) : ∀ (a : βᵐᵒᵖ), (MulEquiv.op f).symm a = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a

@[simp]

theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) : ∀ (a : β), (AddEquiv.op.symm f).symm a = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a

@[simp]

theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : ∀ (a : βᵃᵒᵖ), (AddEquiv.op f).symm a = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a

@[simp]

theorem MulEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) : ∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

@[simp]

theorem MulEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) : ∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

@[simp]

theorem AddEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) : ∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

def MulEquiv.op {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] : α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)

An iso α ≃* β can equivalently be viewed as an iso αᵐᵒᵖ ≃* βᵐᵒᵖ.

Equations

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

def AddEquiv.unop {α : Type u_2} {β : Type u_3} [Add α] [Add β] : αᵃᵒᵖ ≃+ βᵃᵒᵖ ≃ (α ≃+ β)

The 'unopposite' of an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ. Inverse to AddEquiv.op.

Equations

• AddEquiv.unop = AddEquiv.op.symm

def MulEquiv.unop {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] : αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β)

The 'unopposite' of an iso αᵐᵒᵖ ≃* βᵐᵒᵖ. Inverse to MulEquiv.op.

Equations

• MulEquiv.unop = MulEquiv.op.symm

theorem AddMonoidHom.mul_op_ext_iff {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] {f : αᵐᵒᵖ →+ β} {g : αᵐᵒᵖ →+ β} : f = g ↔ f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom

theorem AddMonoidHom.mul_op_ext {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom) : f = g

This ext lemma changes equalities on αᵐᵒᵖ →+ β to equalities on α →+ β. This is useful because there are often ext lemmas for specific αs that will apply to an equality of α →+ β such as Finsupp.addHom_ext'.