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 = let __spread.0 := MulOpposite.instAddCommMonoid; 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 = let __spread.0 := MulOpposite.instAddGroup; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• MulOpposite.instAddCommGroupWithOne = let __spread.0 := MulOpposite.instAddGroupWithOne; 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

• ⋯ = ⋯

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

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 ⋯

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

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

Equations

• MulOpposite.instLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯

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

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 ⋯

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

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

Equations

• MulOpposite.instCommSemigroup = CommSemigroup.mk ⋯

theorem AddOpposite.instAddZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] : ∀ (x : αᵃᵒᵖ), x + 0 = x

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

Equations

• AddOpposite.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

theorem AddOpposite.instAddZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] : ∀ (x : αᵃᵒᵖ), 0 + x = x

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

Equations

• MulOpposite.instMulOneClass = MulOneClass.mk ⋯ ⋯

theorem AddOpposite.instAddMonoid.proof_3 {α : Type u_1} [AddMonoid α] : ∀ (x : αᵃᵒᵖ), (fun (n : ℕ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) 0 x = 0

theorem AddOpposite.instAddMonoid.proof_4 {α : Type u_1} [AddMonoid α] : ∀ (x : ℕ) (x_1 : αᵃᵒᵖ), (fun (n : ℕ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) (x + 1) x_1 = (fun (n : ℕ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) x x_1 + x_1

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

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

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

Equations

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

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

Equations

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

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

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

Equations

• AddOpposite.instAddLeftCancelMonoid = let __spread.0 := AddOpposite.instAddMonoid; AddLeftCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

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

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

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

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

Equations

• MulOpposite.instLeftCancelMonoid = let __spread.0 := MulOpposite.instMonoid; LeftCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

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

Equations

• AddOpposite.instAddRightCancelMonoid = let __spread.0 := AddOpposite.instAddMonoid; AddRightCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

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

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

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

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

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

Equations

• MulOpposite.instRightCancelMonoid = let __spread.0 := MulOpposite.instMonoid; RightCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

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

Equations

• AddOpposite.instAddCancelMonoid = let __spread.0 := AddOpposite.instAddRightCancelMonoid; AddCancelMonoid.mk ⋯

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

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

Equations

• MulOpposite.instCancelMonoid = let __spread.0 := MulOpposite.instRightCancelMonoid; CancelMonoid.mk ⋯

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

Equations

• AddOpposite.instAddCommMonoid = let __spread.0 := AddOpposite.instAddCommSemigroup; AddCommMonoid.mk ⋯

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

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

Equations

• MulOpposite.instCommMonoid = let __spread.0 := MulOpposite.instCommSemigroup; CommMonoid.mk ⋯

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

Equations

• AddOpposite.instAddCancelCommMonoid = let __spread.0 := AddOpposite.instAddCommMonoid; AddCancelCommMonoid.mk ⋯

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

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

Equations

• MulOpposite.instCancelCommMonoid = let __spread.0 := MulOpposite.instCommMonoid; CancelCommMonoid.mk ⋯

theorem AddOpposite.instSubNegMonoid.proof_3 {α : Type u_1} [SubNegMonoid α] : ∀ (x : ℕ) (x_1 : αᵃᵒᵖ), (fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) (Int.ofNat (Nat.succ x)) x_1 = (fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) (Int.ofNat x) x_1 + x_1

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

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

Equations

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

theorem AddOpposite.instSubNegMonoid.proof_4 {α : Type u_1} [SubNegMonoid α] : ∀ (x : ℕ) (x_1 : αᵃᵒᵖ), (fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) (Int.negSucc x) x_1 = -(fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) (↑(Nat.succ x)) x_1

theorem AddOpposite.instSubNegMonoid.proof_2 {α : Type u_1} [SubNegMonoid α] : ∀ (x : αᵃᵒᵖ), (fun (n : ℤ) (a : αᵃᵒᵖ) => AddOpposite.op (n • AddOpposite.unop a)) 0 x = 0

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

Equations

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

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

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

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

Equations

• AddOpposite.instSubtractionMonoid = let __spread.0 := AddOpposite.instInvolutiveNeg; SubtractionMonoid.mk ⋯ ⋯ ⋯

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

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

Equations

• MulOpposite.instDivisionMonoid = let __spread.0 := MulOpposite.instInvolutiveInv; DivisionMonoid.mk ⋯ ⋯ ⋯

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

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

Equations

• AddOpposite.instSubtractionCommMonoid = let __spread.0 := AddOpposite.instAddCommSemigroup; SubtractionCommMonoid.mk ⋯

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

Equations

• MulOpposite.instDivisionCommMonoid = let __spread.0 := MulOpposite.instCommSemigroup; DivisionCommMonoid.mk ⋯

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

Equations

• AddOpposite.instAddGroup = AddGroup.mk ⋯

theorem AddOpposite.instAddGroup.proof_1 {α : Type u_1} [AddGroup α] : ∀ (x : αᵃᵒᵖ), -x + x = 0

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

Equations

• MulOpposite.instGroup = Group.mk ⋯

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

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

Equations

• AddOpposite.instAddCommGroup = let __spread.0 := AddOpposite.instAddCommSemigroup; AddCommGroup.mk ⋯

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

Equations

• MulOpposite.instCommGroup = let __spread.0 := MulOpposite.instCommSemigroup; 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 : ℕ) [Nat.AtLeastTwo n] : AddOpposite.op (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem MulOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [Nat.AtLeastTwo n] : 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 : ℕ) [Nat.AtLeastTwo n] : AddOpposite.unop (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem MulOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [Nat.AtLeastTwo n] : 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 α] : ⇑(AddEquiv.symm MulOpposite.opAddEquiv) = 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 = let __src := MulOpposite.opEquiv; { toEquiv := __src, 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 = let __spread.0 := AddOpposite.instAddCommMonoid; AddCommMonoidWithOne.mk ⋯

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

Equations

• AddOpposite.instAddCommGroupWithOne = let __spread.0 := AddOpposite.instAddCommMonoidWithOne; 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 α] : ⇑(MulEquiv.symm AddOpposite.opMulEquiv) = AddOpposite.unop

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

@[simp]

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

@[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.symm (AddEquiv.neg' G)) = Neg.neg ∘ AddOpposite.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 = let __src := (Equiv.inv G).trans MulOpposite.opEquiv; { toEquiv := __src, 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

• 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 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)) : ⇑(AddHom.toOpposite f hf) = AddOpposite.op ∘ ⇑f

@[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)) : ⇑(MulHom.toOpposite f hf) = MulOpposite.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

• MulHom.toOpposite f 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

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

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

@[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)) : ⇑(MulHom.fromOpposite f hf) = ⇑f ∘ MulOpposite.unop

@[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)) : ⇑(AddHom.fromOpposite f hf) = ⇑f ∘ AddOpposite.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

• MulHom.fromOpposite f 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

• 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)

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

@[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)) : ⇑(AddMonoidHom.toOpposite f 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)) : ⇑(MonoidHom.toOpposite f 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

• MonoidHom.toOpposite f hf = { toOneHom := { 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

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

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

@[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)) : ⇑(MonoidHom.fromOpposite f 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)) : ⇑(AddMonoidHom.fromOpposite f 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

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

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_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_4 {M : Type u_1} [AddMonoid M] (u : AddUnits M) : AddOpposite.op ↑(-u) + AddOpposite.op ↑u = 0

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

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.

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

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

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)ᵃᵒᵖ) : ↑((AddEquiv.symm AddUnits.opEquiv) u) = AddOpposite.op ↑(AddOpposite.unop u)

@[simp]

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

theorem IsAddUnit.op {M : Type u_2} [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_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)

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_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

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

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.

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_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_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_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 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

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

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

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_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_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 }

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)

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_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_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_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_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

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_2) [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_2) [Add M] : ∀ (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.symm (AddEquiv.opOp M)) a = AddOpposite.unop (AddOpposite.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 MulEquiv.opOp_symm_apply (M : Type u_2) [Mul M] : ∀ (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.symm (MulEquiv.opOp M)) a = MulOpposite.unop (MulOpposite.unop a)

@[simp]

theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] : ∀ (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op 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 = let __spread.0 := MulOpposite.opEquiv.trans MulOpposite.opEquiv; { toEquiv := __spread.0, map_mul' := ⋯ }

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

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

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_symm_apply {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : AddEquiv.mulOp f = AddEquiv.trans (AddEquiv.symm MulOpposite.opAddEquiv) (AddEquiv.trans f MulOpposite.opAddEquiv)

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

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_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_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

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.

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_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_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_4 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) : AddOpposite.unop ((AddEquiv.symm f) (f (AddOpposite.op x))) = x

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

@[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_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) : ∀ (a : β), (AddEquiv.symm (AddEquiv.op.symm f)) a = (AddOpposite.unop ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.op) a

@[simp]

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

@[simp]

theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : ∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

@[simp]

theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : ∀ (a : βᵃᵒᵖ), (AddEquiv.symm (AddEquiv.op f)) a = (AddOpposite.op ∘ ⇑(AddEquiv.symm f) ∘ AddOpposite.unop) 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 {α : Type u_2} {β : Type u_3} [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'.