Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

instance AddOpposite.natCast (α : Type u) [inst : NatCast α] :
Equations
instance MulOpposite.natCast (α : Type u) [inst : NatCast α] :
Equations
instance AddOpposite.intCast (α : Type u) [inst : IntCast α] :
Equations
instance MulOpposite.intCast (α : Type u) [inst : IntCast α] :
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance MulOpposite.addMonoid (α : Type u) [inst : AddMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance MulOpposite.addGroup (α : Type u) [inst : AddGroup α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations

Multiplicative structures on αᵐᵒᵖ #

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

Equations
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))
instance MulOpposite.semigroup (α : Type u) [inst : Semigroup α] :
Equations
def AddOpposite.addLeftCancelSemigroup.proof_1 (α : Type u_1) [inst : AddRightCancelSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b + c = a + (b + c)
Equations
def AddOpposite.addLeftCancelSemigroup.proof_2 (α : Type u_1) [inst : AddRightCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2x_1 = x_2
Equations
  • (_ : x = x) = (_ : x = x)
Equations
def AddOpposite.addRightCancelSemigroup.proof_1 (α : Type u_1) [inst : AddLeftCancelSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b + c = a + (b + c)
Equations
def AddOpposite.addRightCancelSemigroup.proof_2 (α : Type u_1) [inst : AddLeftCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1x = x_2
Equations
  • (_ : x = x) = (_ : x = x)
Equations
def AddOpposite.addCommSemigroup.proof_1 (α : Type u_1) [inst : AddCommSemigroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b + c = a + (b + c)
Equations
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)
Equations
def AddOpposite.addZeroClass.proof_1 (α : Type u_1) [inst : AddZeroClass α] (x : αᵃᵒᵖ) :
0 + x = x
Equations
  • (_ : 0 + x = x) = (_ : 0 + x = x)
def AddOpposite.addZeroClass.proof_2 (α : Type u_1) [inst : AddZeroClass α] (x : αᵃᵒᵖ) :
x + 0 = x
Equations
  • (_ : x + 0 = x) = (_ : x + 0 = x)
Equations
Equations
def AddOpposite.addMonoid.proof_3 (α : Type u_1) [inst : AddMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
Equations
def AddOpposite.addMonoid.proof_2 (α : Type u_1) [inst : AddMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
Equations
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.
instance AddOpposite.addMonoid (α : Type u) [inst : AddMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addMonoid.proof_1 (α : Type u_1) [inst : AddMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b + c = a + (b + c)
Equations
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)
instance MulOpposite.monoid (α : Type u) [inst : Monoid α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addLeftCancelMonoid.proof_1 (α : Type u_1) [inst : AddRightCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = a + cb = c
Equations
Equations
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addRightCancelMonoid.proof_1 (α : Type u_1) [inst : AddLeftCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = c + ba = c
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addCancelMonoid.proof_5 (α : Type u_1) [inst : AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = c + ba = c
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addCancelMonoid.proof_2 (α : Type u_1) [inst : AddCancelMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
Equations
def AddOpposite.addCancelMonoid.proof_1 (α : Type u_1) [inst : AddCancelMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
Equations
Equations
def AddOpposite.addCommMonoid.proof_4 (α : Type u_1) [inst : AddCommMonoid α] (n : ) (x : αᵃᵒᵖ) :
Equations
def AddOpposite.addCommMonoid.proof_2 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
Equations
def AddOpposite.addCommMonoid.proof_1 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
Equations
def AddOpposite.addCommMonoid.proof_5 (α : Type u_1) [inst : AddCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
Equations
Equations
instance MulOpposite.commMonoid (α : Type u) [inst : CommMonoid α] :
Equations
def AddOpposite.addCancelCommMonoid.proof_1 (α : Type u_1) [inst : AddCancelCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
def AddOpposite.subNegMonoid.proof_4 (α : Type u_1) [inst : SubNegMonoid α] (n : ) (x : αᵃᵒᵖ) :
Equations
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)
Equations
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)
def AddOpposite.subNegMonoid.proof_1 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
Equations
def AddOpposite.subNegMonoid.proof_5 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b + c = a + (b + c)
Equations
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.
def AddOpposite.subNegMonoid.proof_2 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
Equations
Equations
def AddOpposite.subNegMonoid.proof_7 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
Equations
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.
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)
def AddOpposite.subNegMonoid.proof_6 (α : Type u_1) [inst : SubNegMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
Equations
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.
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.subtractionMonoid.proof_6 (α : Type u_1) [inst : SubtractionMonoid α] :
∀ (x x_1 : αᵃᵒᵖ), -(x + x_1) = -x_1 + -x
Equations
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)
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.subtractionMonoid.proof_1 (α : Type u_1) [inst : SubtractionMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a - b = a + -b
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.subtractionCommMonoid.proof_4 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
Equations
def AddOpposite.subtractionCommMonoid.proof_2 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
-(a + b) = -b + -a
Equations
def AddOpposite.subtractionCommMonoid.proof_3 (α : Type u_1) [inst : SubtractionCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = 0-a = b
Equations
Equations
  • One or more equations did not get rendered due to their size.
def AddOpposite.addGroup.proof_1 (α : Type u_1) [inst : AddGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a - b = a + -b
Equations
def AddOpposite.addGroup.proof_2 (α : Type u_1) [inst : AddGroup α] (a : αᵃᵒᵖ) :
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.addGroup (α : Type u) [inst : AddGroup α] :
Equations
def AddOpposite.addGroup.proof_5 (α : Type u_1) [inst : AddGroup α] (x : αᵃᵒᵖ) :
-x + x = 0
Equations
  • (_ : -x + x = 0) = (_ : -x + x = 0)
instance MulOpposite.group (α : Type u) [inst : Group α] :
Equations
def AddOpposite.addCommGroup.proof_2 (α : Type u_1) [inst : AddCommGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
Equations
def AddOpposite.addCommGroup.proof_1 (α : Type u_1) [inst : AddCommGroup α] (a : αᵃᵒᵖ) :
-a + a = 0
Equations
instance MulOpposite.commGroup (α : Type u) [inst : CommGroup α] :
Equations
@[simp]
theorem AddOpposite.op_natCast {α : Type u} [inst : NatCast α] (n : ) :
{ unop := n } = n
@[simp]
theorem MulOpposite.op_natCast {α : Type u} [inst : NatCast α] (n : ) :
{ unop := n } = n
@[simp]
theorem AddOpposite.op_intCast {α : Type u} [inst : IntCast α] (n : ) :
{ unop := n } = n
@[simp]
theorem MulOpposite.op_intCast {α : Type u} [inst : IntCast α] (n : ) :
{ unop := n } = n
@[simp]
theorem AddOpposite.unop_natCast {α : Type u} [inst : NatCast α] (n : ) :
(n).unop = n
@[simp]
theorem MulOpposite.unop_natCast {α : Type u} [inst : NatCast α] (n : ) :
(n).unop = n
@[simp]
theorem AddOpposite.unop_intCast {α : Type u} [inst : IntCast α] (n : ) :
(n).unop = n
@[simp]
theorem MulOpposite.unop_intCast {α : Type u} [inst : IntCast α] (n : ) :
(n).unop = n
@[simp]
theorem AddOpposite.unop_sub {α : Type u} [inst : SubNegMonoid α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
(x - y).unop = -y.unop + x.unop
@[simp]
theorem MulOpposite.unop_div {α : Type u} [inst : DivInvMonoid α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
(x / y).unop = y.unop⁻¹ * x.unop
@[simp]
theorem AddOpposite.op_sub {α : Type u} [inst : SubNegMonoid α] (x : α) (y : α) :
{ unop := x - y } = -{ unop := y } + { unop := x }
@[simp]
theorem MulOpposite.op_div {α : Type u} [inst : DivInvMonoid α] (x : α) (y : α) :
{ unop := x / y } = { unop := y }⁻¹ * { unop := x }
@[simp]
theorem AddOpposite.semiconjBy_op {α : Type u} [inst : Add α] {a : α} {x : α} {y : α} :
AddSemiconjBy { unop := a } { unop := y } { unop := x } AddSemiconjBy a x y
@[simp]
theorem MulOpposite.semiconjBy_op {α : Type u} [inst : Mul α] {a : α} {x : α} {y : α} :
SemiconjBy { unop := a } { unop := y } { unop := x } SemiconjBy a x y
@[simp]
theorem AddOpposite.semiconjBy_unop {α : Type u} [inst : Add α] {a : αᵃᵒᵖ} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} :
AddSemiconjBy a.unop y.unop x.unop AddSemiconjBy a x y
@[simp]
theorem MulOpposite.semiconjBy_unop {α : Type u} [inst : Mul α] {a : αᵐᵒᵖ} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} :
SemiconjBy a.unop y.unop x.unop SemiconjBy a x y
theorem AddSemiconjBy.op {α : Type u} [inst : Add α] {a : α} {x : α} {y : α} (h : AddSemiconjBy a x y) :
AddSemiconjBy { unop := a } { unop := y } { unop := x }
theorem SemiconjBy.op {α : Type u} [inst : Mul α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) :
SemiconjBy { unop := a } { unop := y } { unop := x }
theorem AddSemiconjBy.unop {α : Type u} [inst : Add α] {a : αᵃᵒᵖ} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} (h : AddSemiconjBy a x y) :
AddSemiconjBy a.unop y.unop x.unop
theorem SemiconjBy.unop {α : Type u} [inst : Mul α] {a : αᵐᵒᵖ} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} (h : SemiconjBy a x y) :
SemiconjBy a.unop y.unop x.unop
theorem AddCommute.op {α : Type u} [inst : Add α] {x : α} {y : α} (h : AddCommute x y) :
AddCommute { unop := x } { unop := y }
theorem Commute.op {α : Type u} [inst : Mul α] {x : α} {y : α} (h : Commute x y) :
Commute { unop := x } { unop := y }
theorem AddOpposite.Commute.unop {α : Type u} [inst : Add α] {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} (h : AddCommute x y) :
AddCommute x.unop y.unop
theorem MulOpposite.Commute.unop {α : Type u} [inst : Mul α] {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} (h : Commute x y) :
Commute x.unop y.unop
@[simp]
theorem AddOpposite.commute_op {α : Type u} [inst : Add α] {x : α} {y : α} :
AddCommute { unop := x } { unop := y } AddCommute x y
@[simp]
theorem MulOpposite.commute_op {α : Type u} [inst : Mul α] {x : α} {y : α} :
Commute { unop := x } { unop := y } Commute x y
@[simp]
theorem AddOpposite.commute_unop {α : Type u} [inst : Add α] {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} :
AddCommute x.unop y.unop AddCommute x y
@[simp]
theorem MulOpposite.commute_unop {α : Type u} [inst : Mul α] {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} :
Commute x.unop y.unop Commute x y
@[simp]
theorem MulOpposite.opAddEquiv_apply {α : Type u} [inst : Add α] :
MulOpposite.opAddEquiv = MulOpposite.op
@[simp]
theorem MulOpposite.opAddEquiv_symm_apply {α : Type u} [inst : Add α] :
↑(AddEquiv.symm MulOpposite.opAddEquiv) = MulOpposite.unop
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.
@[simp]
theorem MulOpposite.opAddEquiv_toEquiv {α : Type u} [inst : Add α] :
MulOpposite.opAddEquiv = MulOpposite.opEquiv

Multiplicative structures on αᵃᵒᵖ #

instance AddOpposite.semigroup (α : Type u) [inst : Semigroup α] :
Equations
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.pow (α : Type u) {β : Type u_1} [inst : Pow α β] :
Equations
@[simp]
theorem AddOpposite.op_pow (α : Type u) {β : Type u_1} [inst : Pow α β] (a : α) (b : β) :
{ unop := a ^ b } = { unop := a } ^ b
@[simp]
theorem AddOpposite.unop_pow (α : Type u) {β : Type u_1} [inst : Pow α β] (a : αᵃᵒᵖ) (b : β) :
(a ^ b).unop = a.unop ^ b
instance AddOpposite.monoid (α : Type u) [inst : Monoid α] :
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.commMonoid (α : Type u) [inst : CommMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.group (α : Type u) [inst : Group α] :
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.commGroup (α : Type u) [inst : CommGroup α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddOpposite.opMulEquiv_apply_unop {α : Type u} [inst : Mul α] (unop : α) :
(AddOpposite.opMulEquiv unop).unop = unop
@[simp]
theorem AddOpposite.opMulEquiv_symm_apply {α : Type u} [inst : Mul α] :
↑(MulEquiv.symm AddOpposite.opMulEquiv) = AddOpposite.unop
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.
@[simp]
theorem AddOpposite.opMulEquiv_toEquiv {α : Type u} [inst : Mul α] :
AddOpposite.opMulEquiv = AddOpposite.opEquiv
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.
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.
def AddEquiv.neg' (G : Type u_1) [inst : SubtractionMonoid 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.
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.
@[simp]
theorem MulEquiv.inv'_apply_unop (G : Type u_1) [inst : DivisionMonoid G] :
∀ (a : G), (↑(MulEquiv.inv' G) a).unop = a⁻¹
@[simp]
theorem AddEquiv.neg'_apply_unop (G : Type u_1) [inst : SubtractionMonoid G] :
∀ (a : G), (↑(AddEquiv.neg' G) a).unop = -a
@[simp]
theorem MulEquiv.inv'_symm_apply (G : Type u_1) [inst : DivisionMonoid G] :
↑(MulEquiv.symm (MulEquiv.inv' G)) = Inv.inv MulOpposite.unop
@[simp]
theorem AddEquiv.neg'_symm_apply (G : Type u_1) [inst : SubtractionMonoid G] :
↑(AddEquiv.symm (AddEquiv.neg' G)) = Neg.neg AddOpposite.unop
def MulEquiv.inv' (G : Type u_1) [inst : DivisionMonoid 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.
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 })
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)) :

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 }) }
@[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
@[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
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)) :

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 }) }
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)) :

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

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
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 })
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)) :

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.
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
@[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
@[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
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)) :

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.
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.
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)) :

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.
@[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
@[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
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)) :

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

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

Equations
  • One or more equations did not get rendered due to their size.
def 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.
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)
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)
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.
def Units.opEquiv {M : Type u_1} [inst : Monoid M] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddUnits.coe_unop_opEquiv {M : Type u_1} [inst : AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :
(AddUnits.opEquiv u).unop = (u).unop
@[simp]
theorem Units.coe_unop_opEquiv {M : Type u_1} [inst : Monoid M] (u : Mᵐᵒᵖˣ) :
(Units.opEquiv u).unop = (u).unop
@[simp]
theorem AddUnits.coe_opEquiv_symm {M : Type u_1} [inst : AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :
↑(↑(AddEquiv.symm AddUnits.opEquiv) u) = { unop := u.unop }
@[simp]
theorem Units.coe_opEquiv_symm {M : Type u_1} [inst : Monoid M] (u : Mˣᵐᵒᵖ) :
↑(↑(MulEquiv.symm Units.opEquiv) u) = { unop := u.unop }
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.
def AddHom.op {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add 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.
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.
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.
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.
@[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
@[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
@[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
@[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
def MulHom.op {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

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

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.unop {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

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

Equations
def MulHom.unop {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.mulUnop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] :

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
def AddMonoidHom.unop {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

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

Equations
def MonoidHom.unop {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
def AddMonoidHom.mulUnop {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] :

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

Equations
@[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))
@[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)
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.
def AddEquiv.mulUnop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] :

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

Equations
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.
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.
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
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.
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
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.
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.
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.
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.
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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.
def AddEquiv.unop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] :

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

Equations
def MulEquiv.unop {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Mul β] :

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

Equations
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'.