Group structures on the multiplicative and additive opposites

Additive structures on αᵐᵒᵖ

ink

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

Equations

• AddOpposite.natCast α = { natCast := fun n => { unop := ↑n } }

ink

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

Equations

• MulOpposite.natCast α = { natCast := fun n => { unop := ↑n } }

ink

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

Equations

• AddOpposite.intCast α = { intCast := fun n => { unop := ↑n } }

ink

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

Equations

• MulOpposite.intCast α = { intCast := fun n => { unop := ↑n } }

ink

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

Equations

• MulOpposite.addSemigroup α = Function.Injective.addSemigroup MulOpposite.unop (_ : Function.Injective MulOpposite.unop) (_ : ∀ (x x_1 : αᵐᵒᵖ), (x + x_1).unop = (x + x_1).unop)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• MulOpposite.addCommSemigroup α = Function.Injective.addCommSemigroup MulOpposite.unop (_ : Function.Injective MulOpposite.unop) (_ : ∀ (x x_1 : αᵐᵒᵖ), (x + x_1).unop = (x + x_1).unop)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• MulOpposite.addMonoidWithOne α = let src := MulOpposite.addMonoid α; let src_1 := MulOpposite.one α; let src_2 := MulOpposite.natCast α; AddMonoidWithOne.mk

ink

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

Equations

• MulOpposite.addCommMonoidWithOne α = let src := MulOpposite.addMonoidWithOne α; let src_1 := MulOpposite.addCommMonoid α; AddCommMonoidWithOne.mk (_ : ∀ (a b : αᵐᵒᵖ), a + b = b + a)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• MulOpposite.addGroupWithOne α = let src := MulOpposite.addMonoidWithOne α; let src_1 := MulOpposite.addGroup α; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : αᵐᵒᵖ), -a + a = 0)

ink

instance MulOpposite.addCommGroupWithOne (α : Type u) [inst : 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

ink

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

Equations

• AddOpposite.addSemigroup α = let src := AddOpposite.add α; AddSemigroup.mk (_ : ∀ (x y z : αᵃᵒᵖ), x + y + z = x + (y + z))

ink

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

Equations

• (_ : x + y + z = x + (y + z)) = (_ : x + y + z = x + (y + z))

ink

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

Equations

• MulOpposite.semigroup α = let src := MulOpposite.mul α; Semigroup.mk (_ : ∀ (x y z : αᵐᵒᵖ), x * y * z = x * (y * z))

ink

def AddOpposite.addLeftCancelSemigroup.proof_1 (α : Type u_1) [inst : AddRightCancelSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c)) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c))

ink

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

Equations

• (_ : x = x) = (_ : x = x)

ink

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

Equations

• AddOpposite.addLeftCancelSemigroup α = let src := AddOpposite.addSemigroup α; AddLeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2 → x_1 = x_2)

ink

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

Equations

• MulOpposite.leftCancelSemigroup α = let src := MulOpposite.semigroup α; LeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵐᵒᵖ), x * x_1 = x * x_2 → x_1 = x_2)

ink

def AddOpposite.addRightCancelSemigroup.proof_1 (α : Type u_1) [inst : AddLeftCancelSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c)) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c))

ink

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

Equations

• AddOpposite.addRightCancelSemigroup α = let src := AddOpposite.addSemigroup α; AddRightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1 → x = x_2)

ink

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

Equations

• (_ : x = x) = (_ : x = x)

ink

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

Equations

• MulOpposite.rightCancelSemigroup α = let src := MulOpposite.semigroup α; RightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵐᵒᵖ), x * x_1 = x_2 * x_1 → x = x_2)

ink

def AddOpposite.addCommSemigroup.proof_1 (α : Type u_1) [inst : AddCommSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c)) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c))

ink

def AddOpposite.addCommSemigroup.proof_2 (α : Type u_1) [inst : AddCommSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : x + y = y + x

Equations

• (_ : x + y = y + x) = (_ : x + y = y + x)

ink

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

Equations

• AddOpposite.addCommSemigroup α = let src := AddOpposite.addSemigroup α; AddCommSemigroup.mk (_ : ∀ (x y : αᵃᵒᵖ), x + y = y + x)

ink

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

Equations

• MulOpposite.commSemigroup α = let src := MulOpposite.semigroup α; CommSemigroup.mk (_ : ∀ (x y : αᵐᵒᵖ), x * y = y * x)

ink

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

Equations

• (_ : 0 + x = x) = (_ : 0 + x = x)

ink

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

Equations

• (_ : x + 0 = x) = (_ : x + 0 = x)

ink

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

Equations

• AddOpposite.addZeroClass α = let src := AddOpposite.add α; let src_1 := AddOpposite.zero α; AddZeroClass.mk (_ : ∀ (x : αᵃᵒᵖ), 0 + x = x) (_ : ∀ (x : αᵃᵒᵖ), x + 0 = x)

ink

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

Equations

• MulOpposite.mulOneClass α = let src := MulOpposite.mul α; let src_1 := MulOpposite.one α; MulOneClass.mk (_ : ∀ (x : αᵐᵒᵖ), 1 * x = x) (_ : ∀ (x : αᵐᵒᵖ), x * 1 = x)

ink

def AddOpposite.addMonoid.proof_3 (α : Type u_1) [inst : AddMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

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

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

def AddOpposite.addMonoid.proof_5 (α : Type u_1) [inst : AddMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) (n + 1) x = x + (fun n x => { unop := n • x.unop }) n x

Equations

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

ink

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

Equations

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

ink

def AddOpposite.addMonoid.proof_1 (α : Type u_1) [inst : AddMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c)) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c))

ink

def AddOpposite.addMonoid.proof_4 (α : Type u_1) [inst : AddMonoid α] (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) 0 x = 0

Equations

• (_ : (fun n x => { unop := n • x.unop }) 0 x = 0) = (_ : (fun n x => { unop := n • x.unop }) 0 x = 0)

ink

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

Equations

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

ink

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

Equations

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

ink

def AddOpposite.addLeftCancelMonoid.proof_1 (α : Type u_1) [inst : AddRightCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b = a + c → b = c

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b = a + c → b = c) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b = a + c → b = c)

ink

def AddOpposite.addLeftCancelMonoid.proof_3 (α : Type u_1) [inst : AddRightCancelMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

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

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

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

Equations

• (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

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

Equations

• (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)

ink

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

Equations

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

ink

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

Equations

• (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

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

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

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

Equations

• (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)

ink

def AddOpposite.addRightCancelMonoid.proof_3 (α : Type u_1) [inst : AddLeftCancelMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

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

Equations

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

ink

def AddOpposite.addRightCancelMonoid.proof_1 (α : Type u_1) [inst : AddLeftCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b = c + b → a = c

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c)

ink

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

Equations

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

ink

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

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c)

ink

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

Equations

• AddOpposite.addCancelMonoid α = let src := AddOpposite.addRightCancelMonoid α; let src_1 := AddOpposite.addLeftCancelMonoid α; AddCancelMonoid.mk (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c)

ink

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

Equations

• (_ : ∀ (x : αᵃᵒᵖ), AddRightCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddRightCancelMonoid.nsmul 0 x = 0)

ink

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

Equations

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

ink

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

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

def AddOpposite.addCancelMonoid.proof_1 (α : Type u_1) [inst : AddCancelMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

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

Equations

• MulOpposite.cancelMonoid α = let src := MulOpposite.rightCancelMonoid α; let src_1 := MulOpposite.leftCancelMonoid α; CancelMonoid.mk (_ : ∀ (a b c : αᵐᵒᵖ), a * b = c * b → a = c)

ink

def AddOpposite.addCommMonoid.proof_4 (α : Type u_1) [inst : AddCommMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def AddOpposite.addCommMonoid.proof_2 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

def AddOpposite.addCommMonoid.proof_1 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

def AddOpposite.addCommMonoid.proof_5 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a) = (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

def AddOpposite.addCommMonoid.proof_3 (α : Type u_1) [inst : AddCommMonoid α] (x : αᵃᵒᵖ) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)

ink

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

Equations

• AddOpposite.addCommMonoid α = let src := AddOpposite.addMonoid α; let src_1 := AddOpposite.addCommSemigroup α; AddCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

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

Equations

• MulOpposite.commMonoid α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.commSemigroup α; CommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

ink

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

Equations

• AddOpposite.addCancelCommMonoid α = let src := AddOpposite.addCancelMonoid α; let src_1 := AddOpposite.addCommMonoid α; AddCancelCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

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

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a) = (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

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

Equations

• MulOpposite.cancelCommMonoid α = let src := MulOpposite.cancelMonoid α; let src_1 := MulOpposite.commMonoid α; CancelCommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

ink

def AddOpposite.subNegMonoid.proof_4 (α : Type u_1) [inst : SubNegMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def AddOpposite.subNegMonoid.proof_11 (α : Type u_1) [inst : SubNegMonoid α] (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) 0 x = 0

Equations

• (_ : (fun n x => { unop := n • x.unop }) 0 x = 0) = (_ : (fun n x => { unop := n • x.unop }) 0 x = 0)

ink

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

Equations

• AddOpposite.subNegMonoid α = let src := AddOpposite.addMonoid α; let src_1 := AddOpposite.neg α; SubNegMonoid.mk fun n x => { unop := n • x.unop }

ink

def AddOpposite.subNegMonoid.proof_8 (α : Type u_1) [inst : SubNegMonoid α] (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) 0 x = 0

Equations

• (_ : ∀ (x : αᵃᵒᵖ), (fun n x => { unop := n • x.unop }) 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), (fun n x => { unop := n • x.unop }) 0 x = 0)

ink

def AddOpposite.subNegMonoid.proof_1 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

def AddOpposite.subNegMonoid.proof_5 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c)) = (_ : ∀ (a b c : αᵃᵒᵖ), a + b + c = a + (b + c))

ink

def AddOpposite.subNegMonoid.proof_13 (α : Type u_1) [inst : SubNegMonoid α] (z : ℕ) (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) (Int.negSucc z) x = -(fun n x => { unop := n • x.unop }) (↑(Nat.succ z)) x

Equations

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

ink

def AddOpposite.subNegMonoid.proof_2 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

def AddOpposite.subNegMonoid.proof_3 (α : Type u_1) [inst : SubNegMonoid α] (x : αᵃᵒᵖ) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)

ink

def AddOpposite.subNegMonoid.proof_7 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) : a + 0 = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a) = (_ : ∀ (a : αᵃᵒᵖ), a + 0 = a)

ink

def AddOpposite.subNegMonoid.proof_12 (α : Type u_1) [inst : SubNegMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) (Int.ofNat (Nat.succ n)) x = x + (fun n x => { unop := n • x.unop }) (Int.ofNat n) x

Equations

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

ink

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

Equations

• (_ : a - b = a - b) = (_ : a - b = a - b)

ink

def AddOpposite.subNegMonoid.proof_6 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) : 0 + a = a

Equations

• (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a) = (_ : ∀ (a : αᵃᵒᵖ), 0 + a = a)

ink

def AddOpposite.subNegMonoid.proof_9 (α : Type u_1) [inst : SubNegMonoid α] (n : ℕ) (x : αᵃᵒᵖ) : (fun n x => { unop := n • x.unop }) (n + 1) x = x + (fun n x => { unop := n • x.unop }) n x

Equations

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

ink

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

Equations

• MulOpposite.divInvMonoid α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.inv α; DivInvMonoid.mk fun n x => { unop := x.unop ^ n }

ink

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

Equations

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

ink

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

Equations

• (_ : -(x + x) = -x + -x) = (_ : -(x + x) = -x + -x)

ink

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

Equations

• (_ : -x = x) = (_ : -x = x)

ink

def AddOpposite.subtractionMonoid.proof_5 (α : Type u_1) [inst : SubtractionMonoid α] (x : αᵃᵒᵖ) : - -x = x

Equations

• (_ : ∀ (x : αᵃᵒᵖ), - -x = x) = (_ : ∀ (x : αᵃᵒᵖ), - -x = x)

ink

def AddOpposite.subtractionMonoid.proof_4 (α : Type u_1) [inst : SubtractionMonoid α] (n : ℕ) (a : αᵃᵒᵖ) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

Equations

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

ink

def AddOpposite.subtractionMonoid.proof_1 (α : Type u_1) [inst : SubtractionMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a - b = a + -b

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a - b = a + -b) = (_ : ∀ (a b : αᵃᵒᵖ), a - b = a + -b)

ink

def AddOpposite.subtractionMonoid.proof_3 (α : Type u_1) [inst : SubtractionMonoid α] (n : ℕ) (a : αᵃᵒᵖ) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

Equations

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

ink

def AddOpposite.subtractionMonoid.proof_2 (α : Type u_1) [inst : SubtractionMonoid α] (a : αᵃᵒᵖ) : SubNegMonoid.zsmul 0 a = 0

Equations

• (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0)

ink

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

Equations

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

ink

def AddOpposite.subtractionCommMonoid.proof_4 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a) = (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

def AddOpposite.subtractionCommMonoid.proof_1 (α : Type u_1) [inst : SubtractionCommMonoid α] (x : αᵃᵒᵖ) : - -x = x

Equations

• (_ : ∀ (x : αᵃᵒᵖ), - -x = x) = (_ : ∀ (x : αᵃᵒᵖ), - -x = x)

ink

def AddOpposite.subtractionCommMonoid.proof_2 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : -(a + b) = -b + -a

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), -(a + b) = -b + -a) = (_ : ∀ (a b : αᵃᵒᵖ), -(a + b) = -b + -a)

ink

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

Equations

• AddOpposite.subtractionCommMonoid α = let src := AddOpposite.subtractionMonoid α; let src_1 := AddOpposite.addCommSemigroup α; SubtractionCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

def AddOpposite.subtractionCommMonoid.proof_3 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = 0 → -a = b

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a + b = 0 → -a = b) = (_ : ∀ (a b : αᵃᵒᵖ), a + b = 0 → -a = b)

ink

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

Equations

• MulOpposite.divisionCommMonoid α = let src := MulOpposite.divisionMonoid α; let src_1 := MulOpposite.commSemigroup α; DivisionCommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

ink

def AddOpposite.addGroup.proof_4 (α : Type u_1) [inst : AddGroup α] (n : ℕ) (a : αᵃᵒᵖ) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

Equations

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

ink

def AddOpposite.addGroup.proof_1 (α : Type u_1) [inst : AddGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a - b = a + -b

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a - b = a + -b) = (_ : ∀ (a b : αᵃᵒᵖ), a - b = a + -b)

ink

def AddOpposite.addGroup.proof_2 (α : Type u_1) [inst : AddGroup α] (a : αᵃᵒᵖ) : SubNegMonoid.zsmul 0 a = 0

Equations

• (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0)

ink

def AddOpposite.addGroup.proof_3 (α : Type u_1) [inst : AddGroup α] (n : ℕ) (a : αᵃᵒᵖ) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

Equations

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

ink

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

Equations

• AddOpposite.addGroup α = let src := AddOpposite.subNegMonoid α; AddGroup.mk (_ : ∀ (x : αᵃᵒᵖ), -x + x = 0)

ink

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

Equations

• (_ : -x + x = 0) = (_ : -x + x = 0)

ink

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

Equations

• MulOpposite.group α = let src := MulOpposite.divInvMonoid α; Group.mk (_ : ∀ (x : αᵐᵒᵖ), x⁻¹ * x = 1)

ink

def AddOpposite.addCommGroup.proof_2 (α : Type u_1) [inst : AddCommGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : a + b = b + a

Equations

• (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a) = (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

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

Equations

• AddOpposite.addCommGroup α = let src := AddOpposite.addGroup α; let src_1 := AddOpposite.addCommMonoid α; AddCommGroup.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)

ink

def AddOpposite.addCommGroup.proof_1 (α : Type u_1) [inst : AddCommGroup α] (a : αᵃᵒᵖ) : -a + a = 0

Equations

• (_ : ∀ (a : αᵃᵒᵖ), -a + a = 0) = (_ : ∀ (a : αᵃᵒᵖ), -a + a = 0)

ink

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

Equations

• MulOpposite.commGroup α = let src := MulOpposite.group α; let src_1 := MulOpposite.commMonoid α; CommGroup.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem AddOpposite.semiconjBy_op {α : Type u} [inst : Add α] {a : α} {x : α} {y : α} : AddSemiconjBy { unop := a } { unop := y } { unop := x } ↔ AddSemiconjBy a x y

ink

@[simp]

theorem MulOpposite.semiconjBy_op {α : Type u} [inst : Mul α] {a : α} {x : α} {y : α} : SemiconjBy { unop := a } { unop := y } { unop := x } ↔ SemiconjBy a x y

ink

@[simp]

theorem AddOpposite.semiconjBy_unop {α : Type u} [inst : Add α] {a : αᵃᵒᵖ} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} : AddSemiconjBy a.unop y.unop x.unop ↔ AddSemiconjBy a x y

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

theorem AddOpposite.commute_op {α : Type u} [inst : Add α] {x : α} {y : α} : AddCommute { unop := x } { unop := y } ↔ AddCommute x y

ink

@[simp]

theorem MulOpposite.commute_op {α : Type u} [inst : Mul α] {x : α} {y : α} : Commute { unop := x } { unop := y } ↔ Commute x y

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

The function MulOpposite.op is an additive equivalence.

Equations

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

ink

@[simp]

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

Multiplicative structures on αᵃᵒᵖ

ink

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

Equations

• AddOpposite.semigroup α = Function.Injective.semigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)

ink

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

Equations

• AddOpposite.leftCancelSemigroup α = Function.Injective.leftCancelSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)

ink

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

Equations

• AddOpposite.rightCancelSemigroup α = Function.Injective.rightCancelSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)

ink

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

Equations

• AddOpposite.commSemigroup α = Function.Injective.commSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)

ink

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

Equations

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

ink

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

Equations

• AddOpposite.pow α = { pow := fun a b => { unop := a.unop ^ b } }

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• AddOpposite.addCommGroupWithOne α = let src := AddOpposite.addCommMonoidWithOne α; let src_1 := AddOpposite.addCommGroup α; let src_2 := AddOpposite.intCast α; AddCommGroupWithOne.mk

ink

@[simp]

theorem AddOpposite.opMulEquiv_apply_unop {α : Type u} [inst : Mul α] (unop : α) : (↑AddOpposite.opMulEquiv unop).unop = unop

ink

@[simp]

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

ink

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

The function AddOpposite.op is a multiplicative equivalence.

Equations

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

ink

@[simp]

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

ink

def AddEquiv.neg'.proof_3 (G : Type u_1) [inst : SubtractionMonoid G] (x : G) (y : G) : Equiv.toFun { toFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun, invFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun) } (x + y) = Equiv.toFun { toFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun, invFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun) } x + Equiv.toFun { toFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun, invFun := (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun) } y

Equations

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

ink

def AddEquiv.neg'.proof_1 (G : Type u_1) [inst : SubtractionMonoid G] : Function.LeftInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun

Equations

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

ink

def AddEquiv.neg' (G : Type u_1) [inst : 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

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

ink

def AddEquiv.neg'.proof_2 (G : Type u_1) [inst : SubtractionMonoid G] : Function.RightInverse (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).invFun (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun

Equations

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

ink

@[simp]

theorem MulEquiv.inv'_apply_unop (G : Type u_1) [inst : DivisionMonoid G] : ∀ (a : G), (↑(MulEquiv.inv' G) a).unop = a⁻¹

ink

@[simp]

theorem AddEquiv.neg'_apply_unop (G : Type u_1) [inst : SubtractionMonoid G] : ∀ (a : G), (↑(AddEquiv.neg' G) a).unop = -a

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

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

ink

def AddHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (↑f x) (↑f y)) (x : M) (y : M) : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y }

Equations

• (_ : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y }) = (_ : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y })

ink

def AddHom.toOpposite {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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' := (_ : ∀ (x y : M), { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y }) }

ink

@[simp]

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

ink

@[simp]

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

ink

def MulHom.toOpposite {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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' := (_ : ∀ (x y : M), { unop := ↑f (x * y) } = { unop := ↑f x } * { unop := ↑f y }) }

ink

def AddHom.fromOpposite {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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' := (_ : ∀ (x x_1 : Mᵃᵒᵖ), ↑f (x_1.unop + x.unop) = (↑f ∘ AddOpposite.unop) x + (↑f ∘ AddOpposite.unop) x_1) }

ink

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

Equations

• (_ : ↑f (x.unop + x.unop) = (↑f ∘ AddOpposite.unop) x + (↑f ∘ AddOpposite.unop) x) = (_ : ↑f (x.unop + x.unop) = (↑f ∘ AddOpposite.unop) x + (↑f ∘ AddOpposite.unop) x)

ink

@[simp]

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

ink

@[simp]

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

ink

def MulHom.fromOpposite {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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' := (_ : ∀ (x x_1 : Mᵐᵒᵖ), ↑f (x_1.unop * x.unop) = (↑f ∘ MulOpposite.unop) x * (↑f ∘ MulOpposite.unop) x_1) }

ink

def AddMonoidHom.toOpposite.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (↑f x) (↑f y)) (x : M) (y : M) : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y }

Equations

• (_ : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y }) = (_ : { unop := ↑f (x + y) } = { unop := ↑f x } + { unop := ↑f y })

ink

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

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

ink

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

Equations

• (_ : { unop := ((AddOpposite.op ∘ ↑f) 0).unop } = { unop := 0.unop }) = (_ : { unop := ((AddOpposite.op ∘ ↑f) 0).unop } = { unop := 0.unop })

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

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

Equations

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

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

def AddUnits.opEquiv.proof_5 {M : Type u_1} [inst : AddMonoid M] (x : AddUnits Mᵃᵒᵖ) : AddOpposite.rec' (fun u => { val := { unop := ↑u }, neg := { unop := ↑(-u) }, val_neg := (_ : { unop := ↑u } + { unop := ↑(-u) } = 0), neg_val := (_ : { unop := ↑(-u) } + { unop := ↑u } = 0) }) ((fun u => { unop := { val := (↑u).unop, neg := (↑(-u)).unop, val_neg := (_ : (↑u).unop + (↑(-u)).unop = 0), neg_val := (_ : (↑(-u)).unop + (↑u).unop = 0) } }) x) = x

Equations

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

ink

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

Equations

• (_ : (↑(-u)).unop + (↑u).unop = 0) = (_ : (↑(-u)).unop + (↑u).unop = 0)

ink

def AddUnits.opEquiv.proof_3 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : { unop := ↑u } + { unop := ↑(-u) } = 0

Equations

• (_ : { unop := ↑u } + { unop := ↑(-u) } = 0) = (_ : { unop := ↑u } + { unop := ↑(-u) } = 0)

ink

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

ink

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

Equations

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

ink

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

Equations

• (_ : (↑u).unop + (↑(-u)).unop = 0) = (_ : (↑u).unop + (↑(-u)).unop = 0)

ink

def AddUnits.opEquiv.proof_4 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : { unop := ↑(-u) } + { unop := ↑u } = 0

Equations

• (_ : { unop := ↑(-u) } + { unop := ↑u } = 0) = (_ : { unop := ↑(-u) } + { unop := ↑u } = 0)

ink

def AddUnits.opEquiv.proof_6 {M : Type u_1} [inst : AddMonoid M] (x : (AddUnits M)ᵃᵒᵖ) : (fun u => { unop := { val := (↑u).unop, neg := (↑(-u)).unop, val_neg := (_ : (↑u).unop + (↑(-u)).unop = 0), neg_val := (_ : (↑(-u)).unop + (↑u).unop = 0) } }) (AddOpposite.rec' (fun u => { val := { unop := ↑u }, neg := { unop := ↑(-u) }, val_neg := (_ : { unop := ↑u } + { unop := ↑(-u) } = 0), neg_val := (_ : { unop := ↑(-u) } + { unop := ↑u } = 0) }) x) = x

Equations

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

ink

def AddHom.op.proof_4 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] : ∀ (x : AddHom Mᵃᵒᵖ Nᵃᵒᵖ), (fun f => { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) y) }) ((fun f => { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_add' := (_ : ∀ (x y : M), ((↑f ∘ AddOpposite.op) (x + y)).unop = { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) y }.unop) }) x) = (fun f => { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) y) }) ((fun f => { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_add' := (_ : ∀ (x y : M), ((↑f ∘ AddOpposite.op) (x + y)).unop = { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) y }.unop) }) x)

Equations

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

ink

def AddHom.op.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] : ∀ (x : AddHom M N), (fun f => { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_add' := (_ : ∀ (x y : M), ((↑f ∘ AddOpposite.op) (x + y)).unop = { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) y }.unop) }) ((fun f => { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) y) }) x) = (fun f => { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_add' := (_ : ∀ (x y : M), ((↑f ∘ AddOpposite.op) (x + y)).unop = { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) y }.unop) }) ((fun f => { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) y) }) x)

Equations

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

Equations

• AddHom.unop = Equiv.symm AddHom.op

ink

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

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

Equations

• MulHom.unop = Equiv.symm MulHom.op

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

Equations

• AddHom.mulUnop = Equiv.symm AddHom.mulOp

ink

def AddMonoidHom.op.proof_4 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (x : M) (y : M) : { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } x + ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } y }.unop

Equations

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

ink

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

Equations

• (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) = (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop })

ink

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

ink

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

Equations

• (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) = (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop)

ink

def AddMonoidHom.op.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) : ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } (x + y) = ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } x + ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } y

Equations

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

ink

def AddMonoidHom.op.proof_6 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] : ∀ (x : Mᵃᵒᵖ →+ Nᵃᵒᵖ), (fun f => { toZeroHom := { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) }, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } (x + y) = ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } x + ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } y) }) ((fun f => { toZeroHom := { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) }, map_add' := (_ : ∀ (x y : M), { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } x + ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } y }.unop) }) x) = (fun f => { toZeroHom := { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) }, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } (x + y) = ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } x + ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } y) }) ((fun f => { toZeroHom := { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) }, map_add' := (_ : ∀ (x y : M), { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } x + ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } y }.unop) }) x)

Equations

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

ink

def AddMonoidHom.op.proof_5 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] : ∀ (x : M →+ N), (fun f => { toZeroHom := { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) }, map_add' := (_ : ∀ (x y : M), { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } x + ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } y }.unop) }) ((fun f => { toZeroHom := { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) }, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } (x + y) = ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } x + ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } y) }) x) = (fun f => { toZeroHom := { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) }, map_add' := (_ : ∀ (x y : M), { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } x + ZeroHom.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, map_zero' := (_ : ((↑f ∘ AddOpposite.op) 0).unop = { unop := 0 }.unop) } y }.unop) }) ((fun f => { toZeroHom := { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) }, map_add' := (_ : ∀ (x y : Mᵃᵒᵖ), ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } (x + y) = ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } x + ZeroHom.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, map_zero' := (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) } y) }) x)

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

Equations

• AddMonoidHom.unop = Equiv.symm AddMonoidHom.op

ink

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

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

Equations

• MonoidHom.unop = Equiv.symm MonoidHom.op

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

Equations

• AddMonoidHom.mulUnop = Equiv.symm AddMonoidHom.mulOp

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

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

ink

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

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

Equations

• AddEquiv.mulUnop = Equiv.symm AddEquiv.mulOp

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• (_ : (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x) = (_ : (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x)

ink

def AddEquiv.op.proof_6 {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) (y : α) : { unop := (AddOpposite.unop ∘ ↑f ∘ AddOpposite.op) (x + y) }.unop = { unop := Equiv.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := (_ : ∀ (x : α), (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x), right_inv := (_ : ∀ (x : β), (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x) } x + Equiv.toFun { toFun := AddOpposite.unop ∘ ↑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.op, left_inv := (_ : ∀ (x : α), (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x), right_inv := (_ : ∀ (x : β), (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x) } y }.unop

Equations

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

ink

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

Equations

• (_ : (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x) = (_ : (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x)

ink

def AddEquiv.op.proof_3 {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : Equiv.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := (_ : ∀ (x : αᵃᵒᵖ), (AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x) = x), right_inv := (_ : ∀ (x : βᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) x) = x) } (x + y) = Equiv.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := (_ : ∀ (x : αᵃᵒᵖ), (AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x) = x), right_inv := (_ : ∀ (x : βᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) x) = x) } x + Equiv.toFun { toFun := AddOpposite.op ∘ ↑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop, left_inv := (_ : ∀ (x : αᵃᵒᵖ), (AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) x) = x), right_inv := (_ : ∀ (x : βᵃᵒᵖ), (AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) ((AddOpposite.op ∘ ↑(AddEquiv.symm f) ∘ AddOpposite.unop) x) = x) } y

Equations

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

ink

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

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

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

ink

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

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

Equations

• AddEquiv.unop = Equiv.symm AddEquiv.op

ink

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

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

Equations

• MulEquiv.unop = Equiv.symm MulEquiv.op

ink

theorem AddMonoidHom.mul_op_ext {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : 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'.