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
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
  • MulOpposite.instAddGroupWithOne = AddGroupWithOne.mk SubNegMonoid.zsmul
Equations

Multiplicative structures on αᵐᵒᵖ #

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

theorem AddOpposite.instAddSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) (z : αᵃᵒᵖ) :
x + y + z = x + (y + z)
Equations
Equations
theorem AddOpposite.instAddLeftCancelSemigroup.proof_1 {α : Type u_1} [AddRightCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2x_1 = x_2
Equations
theorem AddOpposite.instAddRightCancelSemigroup.proof_1 {α : Type u_1} [AddLeftCancelSemigroup α] :
∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1x = x_2
Equations
Equations
Equations
theorem AddOpposite.instAddZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] :
∀ (x : αᵃᵒᵖ), x + 0 = x
Equations
theorem AddOpposite.instAddZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] :
∀ (x : αᵃᵒᵖ), 0 + x = x
Equations
theorem AddOpposite.instAddMonoid.proof_3 {α : Type u_1} [AddMonoid α] :
∀ (x : αᵃᵒᵖ), (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) 0 x = 0
Equations
theorem AddOpposite.instAddMonoid.proof_1 {α : Type u_1} [AddMonoid α] (a : αᵃᵒᵖ) :
0 + a = a
theorem AddOpposite.instAddMonoid.proof_4 {α : Type u_1} [AddMonoid α] :
∀ (x : ) (x_1 : αᵃᵒᵖ), (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) (x + 1) x_1 = (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) x x_1 + x_1
theorem AddOpposite.instAddMonoid.proof_2 {α : Type u_1} [AddMonoid α] (a : αᵃᵒᵖ) :
a + 0 = a
instance MulOpposite.instMonoid {α : Type u_1} [Monoid α] :
Equations
Equations
theorem AddOpposite.instAddLeftCancelMonoid.proof_1 {α : Type u_1} [AddRightCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = a + cb = c
Equations
Equations
theorem AddOpposite.instAddRightCancelMonoid.proof_1 {α : Type u_1} [AddLeftCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = c + ba = c
Equations
Equations
theorem AddOpposite.instAddCancelMonoid.proof_1 {α : Type u_1} [AddCancelMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = c + ba = c
Equations
theorem AddOpposite.instAddCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
Equations
theorem AddOpposite.instAddCancelCommMonoid.proof_1 {α : Type u_1} [AddCancelCommMonoid α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) (c : αᵃᵒᵖ) :
a + b = a + cb = c
Equations
Equations
theorem AddOpposite.instSubNegMonoid.proof_3 {α : Type u_1} [SubNegMonoid α] :
∀ (x : ) (x_1 : αᵃᵒᵖ), (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) (↑x.succ) x_1 = (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) (↑x) x_1 + x_1
Equations
theorem AddOpposite.instSubNegMonoid.proof_4 {α : Type u_1} [SubNegMonoid α] :
∀ (x : ) (x_1 : αᵃᵒᵖ), (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) (Int.negSucc x) x_1 = -(fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) (↑x.succ) x_1
theorem AddOpposite.instSubNegMonoid.proof_2 {α : Type u_1} [SubNegMonoid α] :
∀ (x : αᵃᵒᵖ), (fun (n : ) (a : αᵃᵒᵖ) => AddOpposite.op (n AddOpposite.unop a)) 0 x = 0
theorem AddOpposite.instSubNegMonoid.proof_1 {α : Type u_1} [SubNegMonoid α] :
∀ (a b : αᵃᵒᵖ), a - b = a - b
Equations
theorem AddOpposite.instSubtractionMonoid.proof_2 {α : Type u_1} [SubtractionMonoid α] :
∀ (x x_1 : αᵃᵒᵖ), -(x + x_1) = -x_1 + -x
theorem AddOpposite.instSubtractionMonoid.proof_3 {α : Type u_1} [SubtractionMonoid α] :
∀ (x x_1 : αᵃᵒᵖ), x + x_1 = 0-x = x_1
Equations
Equations
Equations
Equations
Equations
theorem AddOpposite.instAddGroup.proof_1 {α : Type u_1} [AddGroup α] :
∀ (x : αᵃᵒᵖ), -x + x = 0
instance MulOpposite.instGroup {α : Type u_1} [Group α] :
Equations
theorem AddOpposite.instAddCommGroup.proof_1 {α : Type u_1} [AddCommGroup α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
a + b = b + a
Equations
Equations
@[simp]
theorem MulOpposite.op_pow {α : Type u_1} [Monoid α] (x : α) (n : ) :
@[simp]
theorem MulOpposite.unop_pow {α : Type u_1} [Monoid α] (x : αᵐᵒᵖ) (n : ) :
@[simp]
theorem MulOpposite.op_zpow {α : Type u_1} [DivInvMonoid α] (x : α) (z : ) :
@[simp]
theorem MulOpposite.unop_zpow {α : Type u_1} [DivInvMonoid α] (x : αᵐᵒᵖ) (z : ) :
@[simp]
theorem AddOpposite.op_natCast {α : Type u_1} [NatCast α] (n : ) :
AddOpposite.op n = n
@[simp]
theorem MulOpposite.op_natCast {α : Type u_1} [NatCast α] (n : ) :
MulOpposite.op n = n
@[simp]
theorem AddOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem MulOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem AddOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ) :
AddOpposite.op n = n
@[simp]
theorem MulOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ) :
MulOpposite.op n = n
@[simp]
theorem AddOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ) :
@[simp]
theorem MulOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ) :
@[simp]
theorem AddOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem MulOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem AddOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ) :
@[simp]
theorem MulOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ) :
@[simp]
theorem AddOpposite.op_sub {α : Type u_1} [SubNegMonoid α] (x : α) (y : α) :
@[simp]
theorem MulOpposite.op_div {α : Type u_1} [DivInvMonoid α] (x : α) (y : α) :
@[simp]
theorem AddOpposite.addSemiconjBy_op {α : Type u_1} [Add α] {a : α} {x : α} {y : α} :
@[simp]
theorem MulOpposite.semiconjBy_op {α : Type u_1} [Mul α] {a : α} {x : α} {y : α} :
theorem AddSemiconjBy.op {α : Type u_1} [Add α] {a : α} {x : α} {y : α} (h : AddSemiconjBy a x y) :
theorem SemiconjBy.op {α : Type u_1} [Mul α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) :
theorem SemiconjBy.unop {α : Type u_1} [Mul α] {a : αᵐᵒᵖ} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} (h : SemiconjBy a x y) :
theorem AddCommute.op {α : Type u_1} [Add α] {x : α} {y : α} (h : AddCommute x y) :
theorem Commute.op {α : Type u_1} [Mul α] {x : α} {y : α} (h : Commute x y) :
theorem AddCommute.unop {α : Type u_1} [Add α] {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} (h : AddCommute x y) :
theorem Commute.unop {α : Type u_1} [Mul α] {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} (h : Commute x y) :
@[simp]
theorem AddOpposite.addCommute_op {α : Type u_1} [Add α] {x : α} {y : α} :
@[simp]
theorem MulOpposite.commute_op {α : Type u_1} [Mul α] {x : α} {y : α} :
@[simp]
@[simp]
theorem MulOpposite.opAddEquiv_apply {α : Type u_1} [Add α] :
MulOpposite.opAddEquiv = MulOpposite.op
@[simp]
theorem MulOpposite.opAddEquiv_symm_apply {α : Type u_1} [Add α] :
MulOpposite.opAddEquiv.symm = MulOpposite.unop
def MulOpposite.opAddEquiv {α : Type u_1} [Add α] :

The function MulOpposite.op is an additive equivalence.

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

    Multiplicative structures on αᵃᵒᵖ #

    Equations
    Equations
    Equations
    Equations
    Equations
    instance AddOpposite.pow {α : Type u_1} {β : Type u_2} [Pow α β] :
    Equations
    @[simp]
    theorem AddOpposite.op_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
    @[simp]
    theorem AddOpposite.unop_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵃᵒᵖ) (b : β) :
    instance AddOpposite.instMonoid {α : Type u_1} [Monoid α] :
    Equations
    Equations
    Equations
    instance AddOpposite.instGroup {α : Type u_1} [Group α] :
    Equations
    Equations
    Equations
    Equations
    @[simp]
    theorem AddOpposite.opMulEquiv_apply {α : Type u_1} [Mul α] :
    AddOpposite.opMulEquiv = AddOpposite.op
    @[simp]
    theorem AddOpposite.opMulEquiv_symm_apply {α : Type u_1} [Mul α] :
    AddOpposite.opMulEquiv.symm = AddOpposite.unop
    def AddOpposite.opMulEquiv {α : Type u_1} [Mul α] :

    The function AddOpposite.op is a multiplicative equivalence.

    Equations
    • AddOpposite.opMulEquiv = { toEquiv := AddOpposite.opEquiv, map_mul' := }
    Instances For
      @[simp]
      theorem AddOpposite.opMulEquiv_toEquiv {α : Type u_1} [Mul α] :
      AddOpposite.opMulEquiv = AddOpposite.opEquiv

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

      Equations
      Instances For
        theorem AddEquiv.neg'.proof_1 (G : Type u_1) [SubtractionMonoid G] (x : G) (y : G) :
        (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun (x + y) = (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun x + (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun y
        @[simp]
        theorem MulEquiv.inv'_symm_apply (G : Type u_2) [DivisionMonoid G] :
        (MulEquiv.inv' G).symm = Inv.inv MulOpposite.unop
        @[simp]
        theorem AddEquiv.neg'_apply (G : Type u_2) [SubtractionMonoid G] :
        (AddEquiv.neg' G) = AddOpposite.op Neg.neg
        @[simp]
        theorem AddEquiv.neg'_symm_apply (G : Type u_2) [SubtractionMonoid G] :
        (AddEquiv.neg' G).symm = Neg.neg AddOpposite.unop
        @[simp]
        theorem MulEquiv.inv'_apply (G : Type u_2) [DivisionMonoid G] :
        (MulEquiv.inv' G) = MulOpposite.op Inv.inv

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

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

                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
                • f.fromOpposite hf = { toFun := f MulOpposite.unop, map_mul' := }
                Instances For
                  def AddMonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

                  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
                  • f.toOpposite hf = { toFun := AddOpposite.op f, map_zero' := , map_add' := }
                  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_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :
                    (f.toOpposite hf) = AddOpposite.op f
                    @[simp]
                    theorem MonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :
                    (f.toOpposite hf) = MulOpposite.op f
                    def MonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

                    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
                    • f.toOpposite hf = { toFun := MulOpposite.op f, map_one' := , map_mul' := }
                    Instances For
                      def AddMonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

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

                        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
                        • f.fromOpposite hf = { toFun := f MulOpposite.unop, map_one' := , map_mul' := }
                        Instances For
                          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
                            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

                            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_2} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :
                              (AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop u
                              @[simp]
                              theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : Mᵐᵒᵖˣ) :
                              (MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop u
                              @[simp]
                              theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :
                              (AddUnits.opEquiv.symm u) = AddOpposite.op (AddOpposite.unop u)
                              @[simp]
                              theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mˣᵐᵒᵖ) :
                              (Units.opEquiv.symm u) = MulOpposite.op (MulOpposite.unop u)
                              theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :
                              theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :
                              theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) :
                              @[simp]
                              theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :
                              @[simp]
                              theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :
                              @[simp]
                              theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} :
                              def AddHom.op {M : Type u_2} {N : Type u_3} [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_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 }
                                theorem AddHom.op.proof_3 {M : Type u_1} {N : Type u_2} [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_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_4 {M : Type u_1} {N : Type u_2} [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)
                                @[simp]
                                theorem MulHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) :
                                ∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                @[simp]
                                theorem MulHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :
                                ∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                @[simp]
                                theorem AddHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :
                                ∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                @[simp]
                                theorem AddHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) :
                                ∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                def MulHom.op {M : Type u_2} {N : Type u_3} [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_2} {N : Type u_3} [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_2} {N : Type u_3} [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_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :
                                      ∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op f MulOpposite.unop) a
                                      @[simp]
                                      theorem AddHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) :
                                      ∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                      def AddHom.mulOp {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

                                      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_2} {β : Type u_3} [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_6 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                          ∀ (x : Mᵃᵒᵖ →+ Nᵃᵒᵖ), (fun (f : M →+ N) => { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := , map_add' := }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := , map_add' := }) x) = (fun (f : M →+ N) => { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := , map_add' := }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, 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_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
                                          def AddMonoidHom.op {M : Type u_2} {N : Type u_3} [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
                                            theorem AddMonoidHom.op.proof_3 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :
                                            AddOpposite.unop ((f AddOpposite.op) 0) = AddOpposite.unop { unop' := 0 }
                                            theorem AddMonoidHom.op.proof_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_5 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                            ∀ (x : M →+ N), (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := , map_add' := }) ((fun (f : M →+ N) => { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := , map_add' := }) x) = (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, map_zero' := , map_add' := }) ((fun (f : M →+ N) => { toFun := AddOpposite.op f AddOpposite.unop, map_zero' := , map_add' := }) x)
                                            @[simp]
                                            theorem MonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                            ∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                            @[simp]
                                            theorem AddMonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :
                                            ∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                            @[simp]
                                            theorem MonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) :
                                            ∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                            @[simp]
                                            theorem AddMonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                            ∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                            def MonoidHom.op {M : Type u_2} {N : Type u_3} [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_2} {N : Type u_3} [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_2} {N : Type u_3} [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 = { toEquiv := AddOpposite.opEquiv.trans AddOpposite.opEquiv, map_add' := }
                                                  Instances For
                                                    @[simp]
                                                    theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] :
                                                    @[simp]
                                                    theorem AddEquiv.opOp_apply (M : Type u_2) [Add M] :

                                                    A monoid is isomorphic to the opposite of its opposite.

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

                                                      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_2} {β : Type u_3} [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_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :
                                                          AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)
                                                          @[simp]
                                                          theorem AddEquiv.mulOp_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :
                                                          AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)
                                                          def AddEquiv.mulOp {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

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

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

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

                                                            Equations
                                                            • AddEquiv.mulUnop = AddEquiv.mulOp.symm
                                                            Instances For
                                                              def AddEquiv.op {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

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

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem AddEquiv.op.proof_8 {α : Type u_1} {β : Type u_2} [Add α] [Add β] :
                                                                ∀ (x : αᵃᵒᵖ ≃+ βᵃᵒᵖ), (fun (f : α ≃+ β) => { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := , map_add' := }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop f.symm AddOpposite.op, left_inv := , right_inv := , map_add' := }) x) = (fun (f : α ≃+ β) => { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := , map_add' := }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop f.symm AddOpposite.op, left_inv := , right_inv := , map_add' := }) x)
                                                                theorem AddEquiv.op.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) :
                                                                (AddOpposite.op f.symm 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 f.symm AddOpposite.unop) x) = x
                                                                theorem AddEquiv.op.proof_5 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : β) :
                                                                AddOpposite.unop (f (f.symm (AddOpposite.op x))) = x
                                                                theorem AddEquiv.op.proof_4 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) :
                                                                AddOpposite.unop (f.symm (f (AddOpposite.op x))) = x
                                                                theorem AddEquiv.op.proof_7 {α : Type u_1} {β : Type u_2} [Add α] [Add β] :
                                                                ∀ (x : α ≃+ β), (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop f.symm AddOpposite.op, left_inv := , right_inv := , map_add' := }) ((fun (f : α ≃+ β) => { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := , map_add' := }) x) = (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop f.symm AddOpposite.op, left_inv := , right_inv := , map_add' := }) ((fun (f : α ≃+ β) => { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := , map_add' := }) x)
                                                                theorem AddEquiv.op.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
                                                                { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := }.toFun (x + y) = { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := }.toFun x + { toFun := AddOpposite.op f AddOpposite.unop, invFun := AddOpposite.op f.symm AddOpposite.unop, left_inv := , right_inv := }.toFun y
                                                                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 f.symm AddOpposite.op, left_inv := , right_inv := }.toFun x + { toFun := AddOpposite.unop f AddOpposite.op, invFun := AddOpposite.unop f.symm AddOpposite.op, left_inv := , right_inv := }.toFun y }
                                                                @[simp]
                                                                theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :
                                                                ∀ (a : β), (AddEquiv.op.symm f).symm a = (AddOpposite.unop f.symm AddOpposite.op) a
                                                                @[simp]
                                                                theorem MulEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :
                                                                ∀ (a : βᵐᵒᵖ), (MulEquiv.op f).symm a = (MulOpposite.op f.symm MulOpposite.unop) a
                                                                @[simp]
                                                                theorem AddEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :
                                                                ∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop f AddOpposite.op) a
                                                                @[simp]
                                                                theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :
                                                                ∀ (a : β), (MulEquiv.op.symm f).symm a = (MulOpposite.unop f.symm MulOpposite.op) a
                                                                @[simp]
                                                                theorem AddEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :
                                                                ∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op f AddOpposite.unop) a
                                                                @[simp]
                                                                theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :
                                                                ∀ (a : βᵃᵒᵖ), (AddEquiv.op f).symm a = (AddOpposite.op f.symm AddOpposite.unop) a
                                                                @[simp]
                                                                theorem MulEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :
                                                                ∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op f MulOpposite.unop) a
                                                                @[simp]
                                                                theorem MulEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :
                                                                ∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop f MulOpposite.op) a
                                                                def MulEquiv.op {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] :

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

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

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

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

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

                                                                    Equations
                                                                    • MulEquiv.unop = MulEquiv.op.symm
                                                                    Instances For
                                                                      theorem AddMonoidHom.mul_op_ext_iff {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] {f : αᵐᵒᵖ →+ β} {g : αᵐᵒᵖ →+ β} :
                                                                      f = g f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom
                                                                      theorem AddMonoidHom.mul_op_ext {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom) :
                                                                      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'.