Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations

Multiplicative structures on αᵐᵒᵖ #

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

theorem AddOpposite.addSemigroup.proof_1 (α : Type u_1) [AddSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) (z : αᵃᵒᵖ) :
x + y + z = x + (y + z)
theorem AddOpposite.addLeftCancelSemigroup.proof_1 (α : Type u_1) [AddRightCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2x_1 = x_2
theorem AddOpposite.addRightCancelSemigroup.proof_1 (α : Type u_1) [AddLeftCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1x = x_2
theorem AddOpposite.addCommSemigroup.proof_1 (α : Type u_1) [AddCommSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
x + y = y + x
theorem AddOpposite.addZeroClass.proof_2 (α : Type u_1) [AddZeroClass α] (x : αᵃᵒᵖ) :
x + 0 = x
theorem AddOpposite.addZeroClass.proof_1 (α : Type u_1) [AddZeroClass α] (x : αᵃᵒᵖ) :
0 + x = x
Equations
theorem AddOpposite.addMonoid.proof_3 (α : Type u_1) [AddMonoid α] (x : αᵃᵒᵖ) :
(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) 0 x = 0
Equations
  • One or more equations did not get rendered due to their size.
theorem AddOpposite.addMonoid.proof_1 (α : Type u_1) [AddMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
theorem AddOpposite.addMonoid.proof_4 (α : Type u_1) [AddMonoid α] (n : ) (x : αᵃᵒᵖ) :
(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) (n + 1) x = x + (fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) n x
theorem AddOpposite.addMonoid.proof_2 (α : Type u_1) [AddMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
instance MulOpposite.monoid (α : Type u) [Monoid α] :
Equations
theorem AddOpposite.addCancelMonoid.proof_1 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = a + cb = c
theorem AddOpposite.addCancelMonoid.proof_6 (α : Type u_1) [AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = c + ba = c
theorem AddOpposite.addCommMonoid.proof_1 (α : Type u_1) [AddCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
theorem AddOpposite.subNegMonoid.proof_3 (α : Type u_1) [SubNegMonoid α] (n : ) (x : αᵃᵒᵖ) :
(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) (Int.ofNat (Nat.succ n)) x = x + (fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) (Int.ofNat n) x
theorem AddOpposite.subNegMonoid.proof_2 (α : Type u_1) [SubNegMonoid α] (x : αᵃᵒᵖ) :
(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) 0 x = 0
Equations
  • One or more equations did not get rendered due to their size.
theorem AddOpposite.subNegMonoid.proof_4 (α : Type u_1) [SubNegMonoid α] (z : ) (x : αᵃᵒᵖ) :
(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) (Int.negSucc z) x = -(fun (n : ) (x : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop x)) ((Nat.succ z)) x
theorem AddOpposite.subNegMonoid.proof_1 (α : Type u_1) [SubNegMonoid α] :
∀ (a b : αᵃᵒᵖ), a - b = a - b
Equations
theorem AddOpposite.subtractionMonoid.proof_3 (α : Type u_1) [SubtractionMonoid α] :
∀ (x x_1 : αᵃᵒᵖ), x + x_1 = 0-x = x_1
theorem AddOpposite.subtractionMonoid.proof_2 (α : Type u_1) [SubtractionMonoid α] :
∀ (x x_1 : αᵃᵒᵖ), -(x + x_1) = -x_1 + -x
theorem AddOpposite.addGroup.proof_1 (α : Type u_1) [AddGroup α] (x : αᵃᵒᵖ) :
-x + x = 0
instance MulOpposite.group (α : Type u) [Group α] :
Equations
theorem AddOpposite.addCommGroup.proof_1 (α : Type u_1) [AddCommGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
@[simp]
theorem MulOpposite.op_pow {α : Type u} [Monoid α] (x : α) (n : ) :
@[simp]
theorem MulOpposite.unop_pow {α : Type u} [Monoid α] (x : αᵐᵒᵖ) (n : ) :
@[simp]
theorem MulOpposite.op_zpow {α : Type u} [DivInvMonoid α] (x : α) (z : ) :
@[simp]
theorem MulOpposite.unop_zpow {α : Type u} [DivInvMonoid α] (x : αᵐᵒᵖ) (z : ) :
@[simp]
theorem AddOpposite.op_natCast {α : Type u} [NatCast α] (n : ) :
AddOpposite.op n = n
@[simp]
theorem MulOpposite.op_natCast {α : Type u} [NatCast α] (n : ) :
MulOpposite.op n = n
@[simp]
theorem AddOpposite.op_intCast {α : Type u} [IntCast α] (n : ) :
AddOpposite.op n = n
@[simp]
theorem MulOpposite.op_intCast {α : Type u} [IntCast α] (n : ) :
MulOpposite.op n = n
@[simp]
theorem AddOpposite.unop_natCast {α : Type u} [NatCast α] (n : ) :
@[simp]
theorem MulOpposite.unop_natCast {α : Type u} [NatCast α] (n : ) :
@[simp]
theorem AddOpposite.unop_intCast {α : Type u} [IntCast α] (n : ) :
@[simp]
theorem MulOpposite.unop_intCast {α : Type u} [IntCast α] (n : ) :
@[simp]
theorem AddOpposite.op_sub {α : Type u} [SubNegMonoid α] (x : α) (y : α) :
@[simp]
theorem MulOpposite.op_div {α : Type u} [DivInvMonoid α] (x : α) (y : α) :
@[simp]
theorem AddOpposite.addSemiconjBy_op {α : Type u} [Add α] {a : α} {x : α} {y : α} :
@[simp]
theorem MulOpposite.semiconjBy_op {α : Type u} [Mul α] {a : α} {x : α} {y : α} :
theorem AddSemiconjBy.op {α : Type u} [Add α] {a : α} {x : α} {y : α} (h : AddSemiconjBy a x y) :
theorem SemiconjBy.op {α : Type u} [Mul α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) :
theorem AddCommute.op {α : Type u} [Add α] {x : α} {y : α} (h : AddCommute x y) :
theorem Commute.op {α : Type u} [Mul α] {x : α} {y : α} (h : Commute x y) :
theorem Commute.unop {α : Type u} [Mul α] {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} (h : Commute x y) :
@[simp]
theorem AddOpposite.addCommute_op {α : Type u} [Add α] {x : α} {y : α} :
@[simp]
theorem MulOpposite.commute_op {α : Type u} [Mul α] {x : α} {y : α} :
@[simp]
theorem MulOpposite.opAddEquiv_symm_apply {α : Type u} [Add α] :
(AddEquiv.symm MulOpposite.opAddEquiv) = MulOpposite.unop
@[simp]
theorem MulOpposite.opAddEquiv_apply {α : Type u} [Add α] :
MulOpposite.opAddEquiv = MulOpposite.op
def MulOpposite.opAddEquiv {α : Type u} [Add α] :

The function MulOpposite.op is an additive equivalence.

Equations
  • MulOpposite.opAddEquiv = let __src := MulOpposite.opEquiv; { toEquiv := __src, map_add' := }
Instances For
    @[simp]
    theorem MulOpposite.opAddEquiv_toEquiv {α : Type u} [Add α] :
    MulOpposite.opAddEquiv = MulOpposite.opEquiv

    Multiplicative structures on αᵃᵒᵖ #

    instance AddOpposite.pow (α : Type u) {β : Type u_1} [Pow α β] :
    Equations
    @[simp]
    theorem AddOpposite.op_pow (α : Type u) {β : Type u_1} [Pow α β] (a : α) (b : β) :
    @[simp]
    theorem AddOpposite.unop_pow (α : Type u) {β : Type u_1} [Pow α β] (a : αᵃᵒᵖ) (b : β) :
    instance AddOpposite.monoid (α : Type u) [Monoid α] :
    Equations
    Equations
    Equations
    instance AddOpposite.group (α : Type u) [Group α] :
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem AddOpposite.opMulEquiv_apply {α : Type u} [Mul α] :
    AddOpposite.opMulEquiv = AddOpposite.op
    @[simp]
    theorem AddOpposite.opMulEquiv_symm_apply {α : Type u} [Mul α] :
    (MulEquiv.symm AddOpposite.opMulEquiv) = AddOpposite.unop
    def AddOpposite.opMulEquiv {α : Type u} [Mul α] :

    The function AddOpposite.op is a multiplicative equivalence.

    Equations
    • AddOpposite.opMulEquiv = let __src := AddOpposite.opEquiv; { toEquiv := __src, map_mul' := }
    Instances For
      @[simp]
      theorem AddOpposite.opMulEquiv_toEquiv {α : Type u} [Mul α] :
      AddOpposite.opMulEquiv = AddOpposite.opEquiv
      theorem AddEquiv.neg'.proof_1 (G : Type u_1) [SubtractionMonoid G] (x : G) (y : G) :
      ((Equiv.neg G).trans AddOpposite.opEquiv).toFun (x + y) = ((Equiv.neg G).trans AddOpposite.opEquiv).toFun x + ((Equiv.neg G).trans AddOpposite.opEquiv).toFun y

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

      Equations
      Instances For
        @[simp]
        theorem MulEquiv.inv'_apply (G : Type u_1) [DivisionMonoid G] :
        (MulEquiv.inv' G) = MulOpposite.op Inv.inv
        @[simp]
        theorem AddEquiv.neg'_symm_apply (G : Type u_1) [SubtractionMonoid G] :
        (AddEquiv.symm (AddEquiv.neg' G)) = Neg.neg AddOpposite.unop
        @[simp]
        theorem AddEquiv.neg'_apply (G : Type u_1) [SubtractionMonoid G] :
        (AddEquiv.neg' G) = AddOpposite.op Neg.neg
        @[simp]
        theorem MulEquiv.inv'_symm_apply (G : Type u_1) [DivisionMonoid G] :
        (MulEquiv.symm (MulEquiv.inv' G)) = Inv.inv MulOpposite.unop

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

        Equations
        Instances For
          def AddHom.toOpposite {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

          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
          Instances For
            theorem AddHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) (x : M) (y : M) :
            @[simp]
            theorem MulHom.toOpposite_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :
            (MulHom.toOpposite f hf) = MulOpposite.op f
            @[simp]
            theorem AddHom.toOpposite_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
            (AddHom.toOpposite f hf) = AddOpposite.op f
            def MulHom.toOpposite {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

            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
            Instances For
              theorem AddHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
              ∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = (f AddOpposite.unop) x + (f AddOpposite.unop) x_1
              def AddHom.fromOpposite {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

              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
              Instances For
                @[simp]
                theorem AddHom.fromOpposite_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
                (AddHom.fromOpposite f hf) = f AddOpposite.unop
                @[simp]
                theorem MulHom.fromOpposite_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :
                (MulHom.fromOpposite f hf) = f MulOpposite.unop
                def MulHom.fromOpposite {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

                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
                Instances For
                  def AddMonoidHom.toOpposite {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

                  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
                  Instances For
                    theorem AddMonoidHom.toOpposite.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) (x : M) (y : M) :
                    @[simp]
                    theorem AddMonoidHom.toOpposite_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
                    (AddMonoidHom.toOpposite f hf) = AddOpposite.op f
                    @[simp]
                    theorem MonoidHom.toOpposite_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :
                    (MonoidHom.toOpposite f hf) = MulOpposite.op f
                    def MonoidHom.toOpposite {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

                    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
                    Instances For
                      theorem AddMonoidHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
                      ∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = { toFun := f AddOpposite.unop, map_zero' := }.toFun x + { toFun := f AddOpposite.unop, map_zero' := }.toFun x_1
                      def AddMonoidHom.fromOpposite {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

                      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
                      Instances For
                        @[simp]
                        theorem MonoidHom.fromOpposite_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :
                        (MonoidHom.fromOpposite f hf) = f MulOpposite.unop
                        @[simp]
                        theorem AddMonoidHom.fromOpposite_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
                        (AddMonoidHom.fromOpposite f hf) = f AddOpposite.unop
                        def MonoidHom.fromOpposite {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

                        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
                        Instances For
                          theorem AddUnits.opEquiv.proof_7 {M : Type u_1} [AddMonoid M] (x : AddUnits Mᵃᵒᵖ) (y : AddUnits Mᵃᵒᵖ) :
                          { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop u, neg := AddOpposite.unop (-u), val_neg := , neg_val := }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op u, neg := AddOpposite.op (-u), val_neg := , neg_val := }) X, left_inv := , right_inv := }.toFun (x + y) = { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop u, neg := AddOpposite.unop (-u), val_neg := , neg_val := }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op u, neg := AddOpposite.op (-u), val_neg := , neg_val := }) X, left_inv := , right_inv := }.toFun x + { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop u, neg := AddOpposite.unop (-u), val_neg := , neg_val := }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op u, neg := AddOpposite.op (-u), val_neg := , neg_val := }) X, left_inv := , right_inv := }.toFun y
                          theorem AddUnits.opEquiv.proof_5 {M : Type u_1} [AddMonoid M] (x : AddUnits Mᵃᵒᵖ) :
                          (fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op u, neg := AddOpposite.op (-u), val_neg := , neg_val := }) X) ((fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop u, neg := AddOpposite.unop (-u), val_neg := , neg_val := }) x) = x

                          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.
                          Instances For
                            theorem AddUnits.opEquiv.proof_6 {M : Type u_1} [AddMonoid M] (x : (AddUnits M)ᵃᵒᵖ) :
                            (fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop u, neg := AddOpposite.unop (-u), val_neg := , neg_val := }) ((fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op u, neg := AddOpposite.op (-u), val_neg := , neg_val := }) X) x) = x

                            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.
                            Instances For
                              @[simp]
                              theorem AddUnits.coe_unop_opEquiv {M : Type u_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :
                              (AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop u
                              @[simp]
                              theorem Units.coe_unop_opEquiv {M : Type u_1} [Monoid M] (u : Mᵐᵒᵖˣ) :
                              (MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop u
                              @[simp]
                              theorem AddUnits.coe_opEquiv_symm {M : Type u_1} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :
                              ((AddEquiv.symm AddUnits.opEquiv) u) = AddOpposite.op (AddOpposite.unop u)
                              @[simp]
                              theorem Units.coe_opEquiv_symm {M : Type u_1} [Monoid M] (u : Mˣᵐᵒᵖ) :
                              ((MulEquiv.symm Units.opEquiv) u) = MulOpposite.op (MulOpposite.unop u)
                              theorem IsAddUnit.op {M : Type u_1} [AddMonoid M] {m : M} (h : IsAddUnit m) :
                              abbrev IsAddUnit.op.match_1 {M : Type u_1} [AddMonoid M] {m : M} (motive : IsAddUnit mProp) :
                              ∀ (h : IsAddUnit m), (∀ (u : AddUnits M) (hu : u = m), motive )motive h
                              Equations
                              • =
                              Instances For
                                theorem IsUnit.op {M : Type u_1} [Monoid M] {m : M} (h : IsUnit m) :
                                abbrev IsAddUnit.unop.match_1 {M : Type u_1} [AddMonoid M] {m : Mᵃᵒᵖ} (motive : IsAddUnit mProp) :
                                ∀ (h : IsAddUnit m), (∀ (u : AddUnits Mᵃᵒᵖ) (hu : u = m), motive )motive h
                                Equations
                                • =
                                Instances For
                                  theorem IsUnit.unop {M : Type u_1} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) :
                                  @[simp]
                                  theorem isAddUnit_op {M : Type u_1} [AddMonoid M] {m : M} :
                                  @[simp]
                                  theorem isUnit_op {M : Type u_1} [Monoid M] {m : M} :
                                  @[simp]
                                  theorem isUnit_unop {M : Type u_1} [Monoid M] {m : Mᵐᵒᵖ} :
                                  def AddHom.op {M : Type u_1} {N : Type u_2} [Add M] [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.
                                  Instances For
                                    theorem AddHom.op.proof_4 {M : Type u_2} {N : Type u_1} [Add M] [Add N] :
                                    ∀ (x : AddHom Mᵃᵒᵖ Nᵃᵒᵖ), (fun (f : AddHom M N) => { toFun := AddOpposite.op f AddOpposite.unop, map_add' := }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_add' := }) x) = (fun (f : AddHom M N) => { toFun := AddOpposite.op f AddOpposite.unop, map_add' := }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_add' := }) x)
                                    theorem AddHom.op.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) :
                                    (AddOpposite.op f AddOpposite.unop) (x + y) = (AddOpposite.op f AddOpposite.unop) x + (AddOpposite.op f AddOpposite.unop) y
                                    theorem AddHom.op.proof_3 {M : Type u_2} {N : Type u_1} [Add M] [Add N] :
                                    ∀ (x : AddHom M N), (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_add' := }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op f AddOpposite.unop, map_add' := }) x) = (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_add' := }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op f AddOpposite.unop, map_add' := }) x)
                                    theorem AddHom.op.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) (x : M) (y : M) :
                                    AddOpposite.unop ((f AddOpposite.op) (x + y)) = AddOpposite.unop { unop' := (AddOpposite.unop f AddOpposite.op) x + (AddOpposite.unop f AddOpposite.op) y }
                                    @[simp]
                                    theorem AddHom.op_apply_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                                    ∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                    @[simp]
                                    theorem MulHom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :
                                    ∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                    @[simp]
                                    theorem AddHom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) :
                                    ∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                    @[simp]
                                    theorem MulHom.op_apply_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                                    ∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                    def MulHom.op {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :

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

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

                                      Equations
                                      • AddHom.unop = AddHom.op.symm
                                      Instances For
                                        def MulHom.unop {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :

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

                                        Equations
                                        • MulHom.unop = MulHom.op.symm
                                        Instances For
                                          @[simp]
                                          theorem AddHom.mulOp_symm_apply_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) :
                                          ∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                          @[simp]
                                          theorem AddHom.mulOp_apply_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                                          ∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op f MulOpposite.unop) a
                                          def AddHom.mulOp {M : Type u_1} {N : Type u_2} [Add M] [Add N] :

                                          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.
                                          Instances For
                                            def AddHom.mulUnop {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

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

                                            Equations
                                            • AddHom.mulUnop = AddHom.mulOp.symm
                                            Instances For
                                              theorem AddMonoidHom.op.proof_5 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] :
                                              ∀ (x : M →+ N), (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }, map_add' := }) ((fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }, map_add' := }) x) = (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }, map_add' := }) ((fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }, map_add' := }) x)
                                              theorem AddMonoidHom.op.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) :
                                              { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }.toFun (x + y) = { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }.toFun x + { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }.toFun y
                                              theorem AddMonoidHom.op.proof_6 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] :
                                              ∀ (x : Mᵃᵒᵖ →+ Nᵃᵒᵖ), (fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }, map_add' := }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }, map_add' := }) x) = (fun (f : M →+ N) => { toZeroHom := { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := }, map_add' := }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toZeroHom := { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }, map_add' := }) x)
                                              theorem AddMonoidHom.op.proof_4 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (x : M) (y : M) :
                                              AddOpposite.unop { unop' := (AddOpposite.unop f AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }.toFun x + { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := }.toFun y }
                                              theorem AddMonoidHom.op.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                              AddOpposite.op ((f AddOpposite.unop) 0) = AddOpposite.op 0
                                              theorem AddMonoidHom.op.proof_3 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :
                                              AddOpposite.unop ((f AddOpposite.op) 0) = AddOpposite.unop { unop' := 0 }
                                              def AddMonoidHom.op {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

                                              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.
                                              Instances For
                                                @[simp]
                                                theorem AddMonoidHom.op_apply_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                ∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                                @[simp]
                                                theorem MonoidHom.op_apply_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                ∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                                @[simp]
                                                theorem AddMonoidHom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :
                                                ∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                                @[simp]
                                                theorem MonoidHom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) :
                                                ∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                                def MonoidHom.op {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

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

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

                                                  Equations
                                                  • AddMonoidHom.unop = AddMonoidHom.op.symm
                                                  Instances For
                                                    def MonoidHom.unop {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

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

                                                    Equations
                                                    • MonoidHom.unop = MonoidHom.op.symm
                                                    Instances For
                                                      theorem AddEquiv.opOp.proof_1 (M : Type u_1) [Add M] :
                                                      ∀ (x x_1 : M), (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1) = (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1)

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

                                                      Equations
                                                      • AddEquiv.opOp M = let __spread.0 := AddOpposite.opEquiv.trans AddOpposite.opEquiv; { toEquiv := __spread.0, map_add' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem MulEquiv.opOp_apply (M : Type u_1) [Mul M] :
                                                        @[simp]
                                                        theorem AddEquiv.opOp_apply (M : Type u_1) [Add M] :

                                                        A monoid is isomorphic to the opposite of its opposite.

                                                        Equations
                                                        • MulEquiv.opOp M = let __spread.0 := MulOpposite.opEquiv.trans MulOpposite.opEquiv; { toEquiv := __spread.0, map_mul' := }
                                                        Instances For
                                                          @[simp]
                                                          theorem AddMonoidHom.mulOp_apply_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                          ∀ (a : Mᵐᵒᵖ), (AddMonoidHom.mulOp f) a = (MulOpposite.op f MulOpposite.unop) a
                                                          @[simp]
                                                          theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) :
                                                          ∀ (a : M), (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop f MulOpposite.op) a

                                                          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.
                                                          Instances For
                                                            def AddMonoidHom.mulUnop {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] :

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

                                                            Equations
                                                            • AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm
                                                            Instances For
                                                              @[simp]
                                                              theorem AddEquiv.mulOp_symm_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :
                                                              AddEquiv.mulOp.symm f = AddEquiv.trans MulOpposite.opAddEquiv (AddEquiv.trans f (AddEquiv.symm MulOpposite.opAddEquiv))
                                                              @[simp]
                                                              theorem AddEquiv.mulOp_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) :
                                                              AddEquiv.mulOp f = AddEquiv.trans (AddEquiv.symm MulOpposite.opAddEquiv) (AddEquiv.trans f MulOpposite.opAddEquiv)
                                                              def AddEquiv.mulOp {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

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

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

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

                                                                Equations
                                                                • AddEquiv.mulUnop = AddEquiv.mulOp.symm
                                                                Instances For
                                                                  theorem AddEquiv.op.proof_7 {α : Type u_2} {β : Type u_1} [Add α] [Add β] :
                                                                  ∀ (x : α ≃+ β), (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }, map_add' := }) ((fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }, map_add' := }) x) = (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }, map_add' := }) ((fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }, map_add' := }) x)
                                                                  theorem AddEquiv.op.proof_5 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : β) :
                                                                  theorem AddEquiv.op.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) :
                                                                  (AddOpposite.op (AddEquiv.symm f) AddOpposite.unop) ((AddOpposite.op f AddOpposite.unop) x) = x
                                                                  theorem AddEquiv.op.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : α ≃+ β) (x : βᵃᵒᵖ) :
                                                                  (AddOpposite.op f AddOpposite.unop) ((AddOpposite.op (AddEquiv.symm f) AddOpposite.unop) x) = x
                                                                  theorem AddEquiv.op.proof_8 {α : Type u_2} {β : Type u_1} [Add α] [Add β] :
                                                                  ∀ (x : αᵃᵒᵖ ≃+ βᵃᵒᵖ), (fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }, map_add' := }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }, map_add' := }) x) = (fun (f : α ≃+ β) => { toEquiv := { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }, map_add' := }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toEquiv := { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }, map_add' := }) x)
                                                                  theorem AddEquiv.op.proof_6 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) (y : α) :
                                                                  AddOpposite.unop { unop' := (AddOpposite.unop f AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }.toFun x + { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop (AddEquiv.symm f) AddOpposite.op, left_inv := , right_inv := }.toFun y }
                                                                  theorem AddEquiv.op.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
                                                                  { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }.toFun (x + y) = { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }.toFun x + { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op (AddEquiv.symm f) AddOpposite.unop, left_inv := , right_inv := }.toFun y
                                                                  theorem AddEquiv.op.proof_4 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) :
                                                                  def AddEquiv.op {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

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

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem MulEquiv.op_apply_apply {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : α ≃* β) :
                                                                    ∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                                                    @[simp]
                                                                    theorem MulEquiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :
                                                                    ∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                                                    @[simp]
                                                                    theorem AddEquiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) :
                                                                    ∀ (a : βᵃᵒᵖ), (AddEquiv.symm (AddEquiv.op f)) a = (AddOpposite.op (AddEquiv.symm f) AddOpposite.unop) a
                                                                    @[simp]
                                                                    theorem AddEquiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :
                                                                    ∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                                                    @[simp]
                                                                    theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :
                                                                    ∀ (a : β), (MulEquiv.symm (MulEquiv.op.symm f)) a = (MulOpposite.unop (MulEquiv.symm f) MulOpposite.op) a
                                                                    @[simp]
                                                                    theorem AddEquiv.op_apply_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) :
                                                                    ∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                                                    @[simp]
                                                                    theorem MulEquiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : α ≃* β) :
                                                                    ∀ (a : βᵐᵒᵖ), (MulEquiv.symm (MulEquiv.op f)) a = (MulOpposite.op (MulEquiv.symm f) MulOpposite.unop) a
                                                                    @[simp]
                                                                    theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :
                                                                    ∀ (a : β), (AddEquiv.symm (AddEquiv.op.symm f)) a = (AddOpposite.unop (AddEquiv.symm f) AddOpposite.op) a
                                                                    def MulEquiv.op {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] :

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

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def AddEquiv.unop {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

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

                                                                      Equations
                                                                      • AddEquiv.unop = AddEquiv.op.symm
                                                                      Instances For
                                                                        def MulEquiv.unop {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] :

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

                                                                        Equations
                                                                        • MulEquiv.unop = MulEquiv.op.symm
                                                                        Instances For
                                                                          theorem AddMonoidHom.mul_op_ext {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : AddMonoidHom.comp f (AddEquiv.toAddMonoidHom MulOpposite.opAddEquiv) = AddMonoidHom.comp g (AddEquiv.toAddMonoidHom MulOpposite.opAddEquiv)) :
                                                                          f = g

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