Group structures on the multiplicative and additive opposites

Additive structures on αᵐᵒᵖ

instance AddOpposite.natCast (α : Type u) [NatCast α] : NatCast αᵃᵒᵖ

Equations

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

instance MulOpposite.natCast (α : Type u) [NatCast α] : NatCast αᵐᵒᵖ

Equations

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

instance AddOpposite.intCast (α : Type u) [IntCast α] : IntCast αᵃᵒᵖ

Equations

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

instance MulOpposite.intCast (α : Type u) [IntCast α] : IntCast αᵐᵒᵖ

Equations

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

instance MulOpposite.addSemigroup (α : Type u) [AddSemigroup α] : AddSemigroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addLeftCancelSemigroup (α : Type u) [AddLeftCancelSemigroup α] : AddLeftCancelSemigroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addRightCancelSemigroup (α : Type u) [AddRightCancelSemigroup α] : AddRightCancelSemigroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addCommSemigroup (α : Type u) [AddCommSemigroup α] : AddCommSemigroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addZeroClass (α : Type u) [AddZeroClass α] : AddZeroClass αᵐᵒᵖ

Equations

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

instance MulOpposite.addMonoid (α : Type u) [AddMonoid α] : AddMonoid αᵐᵒᵖ

Equations

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

instance MulOpposite.addCommMonoid (α : Type u) [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ

Equations

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

instance MulOpposite.addMonoidWithOne (α : Type u) [AddMonoidWithOne α] : AddMonoidWithOne αᵐᵒᵖ

Equations

• MulOpposite.addMonoidWithOne α = let __src := MulOpposite.addMonoid α; let __src_1 := MulOpposite.one α; let __src_2 := MulOpposite.natCast α; AddMonoidWithOne.mk ⋯ ⋯

instance MulOpposite.addCommMonoidWithOne (α : Type u) [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵐᵒᵖ

Equations

• MulOpposite.addCommMonoidWithOne α = let __src := MulOpposite.addMonoidWithOne α; let __src_1 := MulOpposite.addCommMonoid α; AddCommMonoidWithOne.mk ⋯

instance MulOpposite.subNegMonoid (α : Type u) [SubNegMonoid α] : SubNegMonoid αᵐᵒᵖ

Equations

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

instance MulOpposite.addGroup (α : Type u) [AddGroup α] : AddGroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addCommGroup (α : Type u) [AddCommGroup α] : AddCommGroup αᵐᵒᵖ

Equations

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

instance MulOpposite.addGroupWithOne (α : Type u) [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ

Equations

• MulOpposite.addGroupWithOne α = let __src := MulOpposite.addMonoidWithOne α; let __src_1 := MulOpposite.addGroup α; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.addCommGroupWithOne (α : Type u) [AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ

Equations

• MulOpposite.addCommGroupWithOne α = let __src := MulOpposite.addGroupWithOne α; let __src_1 := MulOpposite.addCommGroup α; AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

Multiplicative structures on αᵐᵒᵖ

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

instance AddOpposite.isAddRightCancel (α : Type u) [Add α] [IsLeftCancelAdd α] : IsRightCancelAdd αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.isRightCancelMul (α : Type u) [Mul α] [IsLeftCancelMul α] : IsRightCancelMul αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance AddOpposite.isAddLeftCancel (α : Type u) [Add α] [IsRightCancelAdd α] : IsLeftCancelAdd αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.isLeftCancelMul (α : Type u) [Mul α] [IsRightCancelMul α] : IsLeftCancelMul αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance AddOpposite.addSemigroup (α : Type u) [AddSemigroup α] : AddSemigroup αᵃᵒᵖ

Equations

• AddOpposite.addSemigroup α = AddSemigroup.mk ⋯

theorem AddOpposite.addSemigroup.proof_1 (α : Type u_1) [AddSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) (z : αᵃᵒᵖ) : x + y + z = x + (y + z)

instance MulOpposite.semigroup (α : Type u) [Semigroup α] : Semigroup αᵐᵒᵖ

Equations

• MulOpposite.semigroup α = Semigroup.mk ⋯

instance AddOpposite.addLeftCancelSemigroup (α : Type u) [AddRightCancelSemigroup α] : AddLeftCancelSemigroup αᵃᵒᵖ

Equations

• AddOpposite.addLeftCancelSemigroup α = AddLeftCancelSemigroup.mk ⋯

theorem AddOpposite.addLeftCancelSemigroup.proof_1 (α : Type u_1) [AddRightCancelSemigroup α] : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2 → x_1 = x_2

instance MulOpposite.leftCancelSemigroup (α : Type u) [RightCancelSemigroup α] : LeftCancelSemigroup αᵐᵒᵖ

Equations

• MulOpposite.leftCancelSemigroup α = LeftCancelSemigroup.mk ⋯

theorem AddOpposite.addRightCancelSemigroup.proof_1 (α : Type u_1) [AddLeftCancelSemigroup α] : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1 → x = x_2

instance AddOpposite.addRightCancelSemigroup (α : Type u) [AddLeftCancelSemigroup α] : AddRightCancelSemigroup αᵃᵒᵖ

Equations

• AddOpposite.addRightCancelSemigroup α = AddRightCancelSemigroup.mk ⋯

instance MulOpposite.rightCancelSemigroup (α : Type u) [LeftCancelSemigroup α] : RightCancelSemigroup αᵐᵒᵖ

Equations

• MulOpposite.rightCancelSemigroup α = RightCancelSemigroup.mk ⋯

instance AddOpposite.addCommSemigroup (α : Type u) [AddCommSemigroup α] : AddCommSemigroup αᵃᵒᵖ

Equations

• AddOpposite.addCommSemigroup α = AddCommSemigroup.mk ⋯

theorem AddOpposite.addCommSemigroup.proof_1 (α : Type u_1) [AddCommSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : x + y = y + x

instance MulOpposite.commSemigroup (α : Type u) [CommSemigroup α] : CommSemigroup αᵐᵒᵖ

Equations

• MulOpposite.commSemigroup α = CommSemigroup.mk ⋯

theorem AddOpposite.addZeroClass.proof_2 (α : Type u_1) [AddZeroClass α] (x : αᵃᵒᵖ) : x + 0 = x

instance AddOpposite.addZeroClass (α : Type u) [AddZeroClass α] : AddZeroClass αᵃᵒᵖ

Equations

• AddOpposite.addZeroClass α = let __src := AddOpposite.add α; let __src_1 := AddOpposite.zero α; AddZeroClass.mk ⋯ ⋯

theorem AddOpposite.addZeroClass.proof_1 (α : Type u_1) [AddZeroClass α] (x : αᵃᵒᵖ) : 0 + x = x

instance MulOpposite.mulOneClass (α : Type u) [MulOneClass α] : MulOneClass αᵐᵒᵖ

Equations

• MulOpposite.mulOneClass α = let __src := MulOpposite.mul α; let __src_1 := MulOpposite.one α; MulOneClass.mk ⋯ ⋯

theorem AddOpposite.addMonoid.proof_3 (α : Type u_1) [AddMonoid α] (x : αᵃᵒᵖ) : (fun (n : ℕ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) 0 x = 0

instance AddOpposite.addMonoid (α : Type u) [AddMonoid α] : AddMonoid αᵃᵒᵖ

Equations

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

theorem AddOpposite.addMonoid.proof_1 (α : Type u_1) [AddMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

theorem AddOpposite.addMonoid.proof_4 (α : Type u_1) [AddMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : (fun (n : ℕ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) (n + 1) x = (fun (n : ℕ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) n x + x

theorem AddOpposite.addMonoid.proof_2 (α : Type u_1) [AddMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

instance MulOpposite.monoid (α : Type u) [Monoid α] : Monoid αᵐᵒᵖ

Equations

• MulOpposite.monoid α = let __src := MulOpposite.semigroup α; let __src_1 := MulOpposite.mulOneClass α; Monoid.mk ⋯ ⋯ (fun (n : ℕ) (x : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop x ^ n)) ⋯ ⋯

theorem AddOpposite.addLeftCancelMonoid.proof_4 (α : Type u_1) [AddRightCancelMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

theorem AddOpposite.addLeftCancelMonoid.proof_3 (α : Type u_1) [AddRightCancelMonoid α] (x : αᵃᵒᵖ) : AddMonoid.nsmul 0 x = 0

theorem AddOpposite.addLeftCancelMonoid.proof_1 (α : Type u_1) [AddRightCancelMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

instance AddOpposite.addLeftCancelMonoid (α : Type u) [AddRightCancelMonoid α] : AddLeftCancelMonoid αᵃᵒᵖ

Equations

• AddOpposite.addLeftCancelMonoid α = let __src := AddOpposite.addLeftCancelSemigroup α; let __src_1 := AddOpposite.addMonoid α; AddLeftCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

theorem AddOpposite.addLeftCancelMonoid.proof_2 (α : Type u_1) [AddRightCancelMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

instance MulOpposite.leftCancelMonoid (α : Type u) [RightCancelMonoid α] : LeftCancelMonoid αᵐᵒᵖ

Equations

• MulOpposite.leftCancelMonoid α = let __src := MulOpposite.leftCancelSemigroup α; let __src_1 := MulOpposite.monoid α; LeftCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

theorem AddOpposite.addRightCancelMonoid.proof_1 (α : Type u_1) [AddLeftCancelMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

theorem AddOpposite.addRightCancelMonoid.proof_4 (α : Type u_1) [AddLeftCancelMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

instance AddOpposite.addRightCancelMonoid (α : Type u) [AddLeftCancelMonoid α] : AddRightCancelMonoid αᵃᵒᵖ

Equations

• AddOpposite.addRightCancelMonoid α = let __src := AddOpposite.addRightCancelSemigroup α; let __src_1 := AddOpposite.addMonoid α; AddRightCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

theorem AddOpposite.addRightCancelMonoid.proof_3 (α : Type u_1) [AddLeftCancelMonoid α] (x : αᵃᵒᵖ) : AddMonoid.nsmul 0 x = 0

theorem AddOpposite.addRightCancelMonoid.proof_2 (α : Type u_1) [AddLeftCancelMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

instance MulOpposite.rightCancelMonoid (α : Type u) [LeftCancelMonoid α] : RightCancelMonoid αᵐᵒᵖ

Equations

• MulOpposite.rightCancelMonoid α = let __src := MulOpposite.rightCancelSemigroup α; let __src_1 := MulOpposite.monoid α; RightCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

theorem AddOpposite.addCancelMonoid.proof_1 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b = a + c → b = c

theorem AddOpposite.addCancelMonoid.proof_4 (α : Type u_1) [AddCancelMonoid α] (x : αᵃᵒᵖ) : AddRightCancelMonoid.nsmul 0 x = 0

theorem AddOpposite.addCancelMonoid.proof_6 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b = c + b → a = c

theorem AddOpposite.addCancelMonoid.proof_3 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

instance AddOpposite.addCancelMonoid (α : Type u) [AddCancelMonoid α] : AddCancelMonoid αᵃᵒᵖ

Equations

• AddOpposite.addCancelMonoid α = let __src := AddOpposite.addRightCancelMonoid α; let __src_1 := AddOpposite.addLeftCancelMonoid α; AddCancelMonoid.mk ⋯

theorem AddOpposite.addCancelMonoid.proof_5 (α : Type u_1) [AddCancelMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : AddRightCancelMonoid.nsmul (n + 1) x = AddRightCancelMonoid.nsmul n x + x

theorem AddOpposite.addCancelMonoid.proof_2 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

instance MulOpposite.cancelMonoid (α : Type u) [CancelMonoid α] : CancelMonoid αᵐᵒᵖ

Equations

• MulOpposite.cancelMonoid α = let __src := MulOpposite.rightCancelMonoid α; let __src_1 := MulOpposite.leftCancelMonoid α; CancelMonoid.mk ⋯

theorem AddOpposite.addCommMonoid.proof_1 (α : Type u_1) [AddCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

instance AddOpposite.addCommMonoid (α : Type u) [AddCommMonoid α] : AddCommMonoid αᵃᵒᵖ

Equations

• AddOpposite.addCommMonoid α = let __src := AddOpposite.addMonoid α; let __src_1 := AddOpposite.addCommSemigroup α; AddCommMonoid.mk ⋯

instance MulOpposite.commMonoid (α : Type u) [CommMonoid α] : CommMonoid αᵐᵒᵖ

Equations

• MulOpposite.commMonoid α = let __src := MulOpposite.monoid α; let __src_1 := MulOpposite.commSemigroup α; CommMonoid.mk ⋯

theorem AddOpposite.addCancelCommMonoid.proof_1 (α : Type u_1) [AddCancelCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

instance AddOpposite.addCancelCommMonoid (α : Type u) [AddCancelCommMonoid α] : AddCancelCommMonoid αᵃᵒᵖ

Equations

• AddOpposite.addCancelCommMonoid α = let __src := AddOpposite.addCancelMonoid α; let __src_1 := AddOpposite.addCommMonoid α; AddCancelCommMonoid.mk ⋯

instance MulOpposite.cancelCommMonoid (α : Type u) [CancelCommMonoid α] : CancelCommMonoid αᵐᵒᵖ

Equations

• MulOpposite.cancelCommMonoid α = let __src := MulOpposite.cancelMonoid α; let __src_1 := MulOpposite.commMonoid α; CancelCommMonoid.mk ⋯

theorem AddOpposite.subNegMonoid.proof_3 (α : Type u_1) [SubNegMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : (fun (n : ℤ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) (Int.ofNat (Nat.succ n)) x = (fun (n : ℤ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) (Int.ofNat n) x + x

theorem AddOpposite.subNegMonoid.proof_2 (α : Type u_1) [SubNegMonoid α] (x : αᵃᵒᵖ) : (fun (n : ℤ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) 0 x = 0

instance AddOpposite.subNegMonoid (α : Type u) [SubNegMonoid α] : SubNegMonoid αᵃᵒᵖ

Equations

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

theorem AddOpposite.subNegMonoid.proof_4 (α : Type u_1) [SubNegMonoid α] (z : ℕ) (x : αᵃᵒᵖ) : (fun (n : ℤ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) (Int.negSucc z) x = -(fun (n : ℤ) (x : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop x)) (↑(Nat.succ z)) x

theorem AddOpposite.subNegMonoid.proof_1 (α : Type u_1) [SubNegMonoid α] : ∀ (a b : αᵃᵒᵖ), a - b = a - b

instance MulOpposite.divInvMonoid (α : Type u) [DivInvMonoid α] : DivInvMonoid αᵐᵒᵖ

Equations

• MulOpposite.divInvMonoid α = let __src := MulOpposite.monoid α; let __src_1 := MulOpposite.inv α; DivInvMonoid.mk ⋯ (fun (n : ℤ) (x : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop x ^ n)) ⋯ ⋯ ⋯

theorem AddOpposite.subtractionMonoid.proof_3 (α : Type u_1) [SubtractionMonoid α] : ∀ (x x_1 : αᵃᵒᵖ), x + x_1 = 0 → -x = x_1

instance AddOpposite.subtractionMonoid (α : Type u) [SubtractionMonoid α] : SubtractionMonoid αᵃᵒᵖ

Equations

• AddOpposite.subtractionMonoid α = let __src := AddOpposite.subNegMonoid α; let __src_1 := AddOpposite.involutiveNeg α; SubtractionMonoid.mk ⋯ ⋯ ⋯

theorem AddOpposite.subtractionMonoid.proof_1 (α : Type u_1) [SubtractionMonoid α] (x : αᵃᵒᵖ) : - -x = x

theorem AddOpposite.subtractionMonoid.proof_2 (α : Type u_1) [SubtractionMonoid α] : ∀ (x x_1 : αᵃᵒᵖ), -(x + x_1) = -x_1 + -x

instance MulOpposite.divisionMonoid (α : Type u) [DivisionMonoid α] : DivisionMonoid αᵐᵒᵖ

Equations

• MulOpposite.divisionMonoid α = let __src := MulOpposite.divInvMonoid α; let __src_1 := MulOpposite.involutiveInv α; DivisionMonoid.mk ⋯ ⋯ ⋯

instance AddOpposite.subtractionCommMonoid (α : Type u) [SubtractionCommMonoid α] : SubtractionCommMonoid αᵃᵒᵖ

Equations

• AddOpposite.subtractionCommMonoid α = let __src := AddOpposite.subtractionMonoid α; let __src_1 := AddOpposite.addCommSemigroup α; SubtractionCommMonoid.mk ⋯

theorem AddOpposite.subtractionCommMonoid.proof_1 (α : Type u_1) [SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

instance MulOpposite.divisionCommMonoid (α : Type u) [DivisionCommMonoid α] : DivisionCommMonoid αᵐᵒᵖ

Equations

• MulOpposite.divisionCommMonoid α = let __src := MulOpposite.divisionMonoid α; let __src_1 := MulOpposite.commSemigroup α; DivisionCommMonoid.mk ⋯

theorem AddOpposite.addGroup.proof_1 (α : Type u_1) [AddGroup α] (x : αᵃᵒᵖ) : -x + x = 0

instance AddOpposite.addGroup (α : Type u) [AddGroup α] : AddGroup αᵃᵒᵖ

Equations

• AddOpposite.addGroup α = let __src := AddOpposite.subNegMonoid α; AddGroup.mk ⋯

instance MulOpposite.group (α : Type u) [Group α] : Group αᵐᵒᵖ

Equations

• MulOpposite.group α = let __src := MulOpposite.divInvMonoid α; Group.mk ⋯

instance AddOpposite.addCommGroup (α : Type u) [AddCommGroup α] : AddCommGroup αᵃᵒᵖ

Equations

• AddOpposite.addCommGroup α = let __src := AddOpposite.addGroup α; let __src_1 := AddOpposite.addCommMonoid α; AddCommGroup.mk ⋯

theorem AddOpposite.addCommGroup.proof_1 (α : Type u_1) [AddCommGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

instance MulOpposite.commGroup (α : Type u) [CommGroup α] : CommGroup αᵐᵒᵖ

Equations

• MulOpposite.commGroup α = let __src := MulOpposite.group α; let __src_1 := MulOpposite.commMonoid α; CommGroup.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem AddOpposite.addSemiconjBy_op {α : Type u} [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} [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} [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} [Mul α] {a : αᵐᵒᵖ} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} : SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x) ↔ SemiconjBy a x y

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulOpposite.opAddEquiv_symm_apply {α : Type u} [Add α] : ⇑(AddEquiv.symm MulOpposite.opAddEquiv) = MulOpposite.unop

@[simp]

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

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

The function MulOpposite.op is an additive equivalence.

Equations

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

@[simp]

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

Multiplicative structures on αᵃᵒᵖ

instance AddOpposite.semigroup (α : Type u) [Semigroup α] : Semigroup αᵃᵒᵖ

Equations

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

instance AddOpposite.leftCancelSemigroup (α : Type u) [LeftCancelSemigroup α] : LeftCancelSemigroup αᵃᵒᵖ

Equations

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

instance AddOpposite.rightCancelSemigroup (α : Type u) [RightCancelSemigroup α] : RightCancelSemigroup αᵃᵒᵖ

Equations

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

instance AddOpposite.commSemigroup (α : Type u) [CommSemigroup α] : CommSemigroup αᵃᵒᵖ

Equations

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

instance AddOpposite.mulOneClass (α : Type u) [MulOneClass α] : MulOneClass αᵃᵒᵖ

Equations

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

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

Equations

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

@[simp]

theorem AddOpposite.op_pow (α : Type u) {β : Type u_1} [Pow α β] (a : α) (b : β) : AddOpposite.op (a ^ b) = AddOpposite.op a ^ b

@[simp]

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

instance AddOpposite.monoid (α : Type u) [Monoid α] : Monoid αᵃᵒᵖ

Equations

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

instance AddOpposite.commMonoid (α : Type u) [CommMonoid α] : CommMonoid αᵃᵒᵖ

Equations

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

instance AddOpposite.divInvMonoid (α : Type u) [DivInvMonoid α] : DivInvMonoid αᵃᵒᵖ

Equations

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

instance AddOpposite.group (α : Type u) [Group α] : Group αᵃᵒᵖ

Equations

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

instance AddOpposite.commGroup (α : Type u) [CommGroup α] : CommGroup αᵃᵒᵖ

Equations

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

instance AddOpposite.addCommMonoidWithOne (α : Type u) [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵃᵒᵖ

Equations

• AddOpposite.addCommMonoidWithOne α = let __src := AddOpposite.addCommMonoid α; let __src_1 := AddOpposite.one; let __src_2 := AddOpposite.natCast α; AddCommMonoidWithOne.mk ⋯

instance AddOpposite.addCommGroupWithOne (α : Type u) [AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ

Equations

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

@[simp]

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

@[simp]

theorem AddOpposite.opMulEquiv_symm_apply {α : Type u} [Mul α] : ⇑(MulEquiv.symm AddOpposite.opMulEquiv) = AddOpposite.unop

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

The function AddOpposite.op is a multiplicative equivalence.

Equations

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

@[simp]

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

theorem AddEquiv.neg'.proof_1 (G : Type u_1) [SubtractionMonoid G] (x : G) (y : G) : ((Equiv.neg G).trans AddOpposite.opEquiv).toFun (x + y) = ((Equiv.neg G).trans AddOpposite.opEquiv).toFun x + ((Equiv.neg G).trans AddOpposite.opEquiv).toFun y

def AddEquiv.neg' (G : Type u_1) [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 = let __src := (Equiv.neg G).trans AddOpposite.opEquiv; { toEquiv := __src, map_add' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def MulEquiv.inv' (G : Type u_1) [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 = let __src := (Equiv.inv G).trans MulOpposite.opEquiv; { toEquiv := __src, map_mul' := ⋯ }

def AddHom.toOpposite {M : Type u_1} {N : Type u_2} [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

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

theorem AddHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) (x : M) (y : M) : AddOpposite.op (f (x + y)) = AddOpposite.op (f x) + AddOpposite.op (f y)

@[simp]

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

@[simp]

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

def MulHom.toOpposite {M : Type u_1} {N : Type u_2} [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

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

theorem AddHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = (⇑f ∘ AddOpposite.unop) x + (⇑f ∘ AddOpposite.unop) x_1

def AddHom.fromOpposite {M : Type u_1} {N : Type u_2} [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

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

@[simp]

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

@[simp]

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

def MulHom.fromOpposite {M : Type u_1} {N : Type u_2} [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

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

theorem AddMonoidHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : AddOpposite.op (f 0) = AddOpposite.op 0

def AddMonoidHom.toOpposite {M : Type u_1} {N : Type u_2} [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

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

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

@[simp]

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

@[simp]

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

def MonoidHom.toOpposite {M : Type u_1} {N : Type u_2} [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

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

theorem AddMonoidHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x + { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x_1

def AddMonoidHom.fromOpposite {M : Type u_1} {N : Type u_2} [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

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

@[simp]

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

@[simp]

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

def MonoidHom.fromOpposite {M : Type u_1} {N : Type u_2} [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

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

theorem AddUnits.opEquiv.proof_4 {M : Type u_1} [AddMonoid M] (u : AddUnits M) : AddOpposite.op ↑(-u) + AddOpposite.op ↑u = 0

theorem AddUnits.opEquiv.proof_7 {M : Type u_1} [AddMonoid M] (x : AddUnits Mᵃᵒᵖ) (y : AddUnits Mᵃᵒᵖ) : { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun y

theorem AddUnits.opEquiv.proof_3 {M : Type u_1} [AddMonoid M] (u : AddUnits M) : AddOpposite.op ↑u + AddOpposite.op ↑(-u) = 0

theorem AddUnits.opEquiv.proof_5 {M : Type u_1} [AddMonoid M] (x : AddUnits Mᵃᵒᵖ) : (fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X) ((fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }) x) = x

def AddUnits.opEquiv {M : Type u_1} [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.

theorem AddUnits.opEquiv.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) : AddOpposite.unop ↑u + AddOpposite.unop ↑(-u) = 0

theorem AddUnits.opEquiv.proof_6 {M : Type u_1} [AddMonoid M] (x : (AddUnits M)ᵃᵒᵖ) : (fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }) ((fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X) x) = x

theorem AddUnits.opEquiv.proof_2 {M : Type u_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) : AddOpposite.unop ↑(-u) + AddOpposite.unop ↑u = 0

def Units.opEquiv {M : Type u_1} [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_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) : ↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u

@[simp]

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

@[simp]

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

@[simp]

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

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

abbrev IsAddUnit.op.match_1 {M : Type u_1} [AddMonoid M] {m : M} (motive : IsAddUnit m → Prop) : ∀ (h : IsAddUnit m), (∀ (u : AddUnits M) (hu : ↑u = m), motive ⋯) → motive h

Equations

• ⋯ = ⋯

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

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

abbrev IsAddUnit.unop.match_1 {M : Type u_1} [AddMonoid M] {m : Mᵃᵒᵖ} (motive : IsAddUnit m → Prop) : ∀ (h : IsAddUnit m), (∀ (u : AddUnits Mᵃᵒᵖ) (hu : ↑u = m), motive ⋯) → motive h

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def AddHom.op {M : Type u_1} {N : Type u_2} [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.

theorem AddHom.op.proof_4 {M : Type u_2} {N : Type u_1} [Add M] [Add N] : ∀ (x : AddHom Mᵃᵒᵖ Nᵃᵒᵖ), (fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) x) = (fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) x)

theorem AddHom.op.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) : (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) y

theorem AddHom.op.proof_3 {M : Type u_2} {N : Type u_1} [Add M] [Add N] : ∀ (x : AddHom M N), (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) x) = (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) x)

theorem AddHom.op.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) (x : M) (y : M) : AddOpposite.unop ((⇑f ∘ AddOpposite.op) (x + y)) = AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) y }

@[simp]

theorem AddHom.op_apply_apply {M : Type u_1} {N : Type u_2} [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_1} {N : Type u_2} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) : ∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

@[simp]

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

@[simp]

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

def MulHom.op {M : Type u_1} {N : Type u_2} [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_1} {N : Type u_2} [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_1} {N : Type u_2} [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_symm_apply_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) : ∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

@[simp]

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

def AddHom.mulOp {M : Type u_1} {N : Type u_2} [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_1} {β : Type u_2} [Add α] [Add β] : AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β

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

Equations

• AddHom.mulUnop = AddHom.mulOp.symm

theorem AddMonoidHom.op.proof_5 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] : ∀ (x : M →+ N), (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }, map_add' := ⋯ }) ((fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }, map_add' := ⋯ }) x) = (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }, map_add' := ⋯ }) ((fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }, map_add' := ⋯ }) x)

theorem AddMonoidHom.op.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) : { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun (x + y) = { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x + { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun y

theorem AddMonoidHom.op.proof_6 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] : ∀ (x : Mᵃᵒᵖ →+ Nᵃᵒᵖ), (fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }, map_add' := ⋯ }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }, map_add' := ⋯ }) x) = (fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }, map_add' := ⋯ }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }, map_add' := ⋯ }) x)

theorem AddMonoidHom.op.proof_4 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (x : M) (y : M) : AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }.toFun x + { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }.toFun y }

theorem AddMonoidHom.op.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : AddOpposite.op ((⇑f ∘ AddOpposite.unop) 0) = AddOpposite.op 0

theorem AddMonoidHom.op.proof_3 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) : AddOpposite.unop ((⇑f ∘ AddOpposite.op) 0) = AddOpposite.unop { unop' := 0 }

def AddMonoidHom.op {M : Type u_1} {N : Type u_2} [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_apply_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : ∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidHom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [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_1} {N : Type u_2} [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_1} {N : Type u_2} [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_1} {N : Type u_2} [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

theorem AddEquiv.opOp.proof_1 (M : Type u_1) [Add M] : ∀ (x x_1 : M), (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1) = (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A monoid is isomorphic to the opposite of its opposite.

Equations

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

@[simp]

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

@[simp]

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

def AddMonoidHom.mulOp {M : Type u_1} {N : Type u_2} [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_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] : (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)

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

Equations

• AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm

@[simp]

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

@[simp]

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

def AddEquiv.mulOp {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [Add α] [Add β] : αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)

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

Equations

• AddEquiv.mulUnop = AddEquiv.mulOp.symm

theorem AddEquiv.op.proof_7 {α : Type u_2} {β : Type u_1} [Add α] [Add β] : ∀ (x : α ≃+ β), (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) ((fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) x) = (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) ((fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) x)

theorem AddEquiv.op.proof_5 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : β) : AddOpposite.unop (f ((AddEquiv.symm f) (AddOpposite.op x))) = x

theorem AddEquiv.op.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) : (AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop) ((AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) x) = x

theorem AddEquiv.op.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : α ≃+ β) (x : βᵃᵒᵖ) : (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) ((AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop) x) = x

theorem AddEquiv.op.proof_8 {α : Type u_2} {β : Type u_1} [Add α] [Add β] : ∀ (x : αᵃᵒᵖ ≃+ βᵃᵒᵖ), (fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) x) = (fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }) x)

theorem AddEquiv.op.proof_6 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) (y : α) : AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }.toFun y }

theorem AddEquiv.op.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun y

theorem AddEquiv.op.proof_4 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) : AddOpposite.unop ((AddEquiv.symm f) (f (AddOpposite.op x))) = x

def AddEquiv.op {α : Type u_1} {β : Type u_2} [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_apply_apply {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : α ≃* β) : ∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def MulEquiv.op {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [Add α] [Add β] : αᵃᵒᵖ ≃+ βᵃᵒᵖ ≃ (α ≃+ β)

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

Equations

• AddEquiv.unop = AddEquiv.op.symm

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

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

Equations

• MulEquiv.unop = MulEquiv.op.symm

theorem AddMonoidHom.mul_op_ext {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : AddMonoidHom.comp f (AddEquiv.toAddMonoidHom MulOpposite.opAddEquiv) = AddMonoidHom.comp g (AddEquiv.toAddMonoidHom MulOpposite.opAddEquiv)) : 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'.