Documentation

Mathlib.Algebra.Group.Equiv.Opposite

Group isomorphism between a group and its opposite #

source
šŸ”ø coverage
def MulOpposite.opMulEquiv {M : Type u_1} [CommMonoid M] :
M ā‰ƒ* Mįµįµ’įµ–

MulOpposite.op on a commutative monoid is an isomorphism.

Instances For
    source
    šŸ”ø coverage
    def AddOpposite.opAddEquiv {M : Type u_1} [AddCommMonoid M] :
    M ā‰ƒ+ Mįµƒįµ’įµ–

    AddOpposite.op on a commutative additive monoid is an isomorphism.

    Instances For
      source
      šŸ“ coverage
      @[simp]
      theorem MulOpposite.opMulEquiv_symm_apply {M : Type u_1} [CommMonoid M] (aāœ : Mįµįµ’įµ–) :
      opMulEquiv.symm aāœ = unop aāœ
      source
      šŸ“ coverage
      @[simp]
      theorem AddOpposite.opAddEquiv_apply {M : Type u_1} [AddCommMonoid M] (aāœ : M) :
      opAddEquiv aāœ = op aāœ
      source
      šŸ“ coverage
      @[simp]
      theorem MulOpposite.opMulEquiv_apply {M : Type u_1} [CommMonoid M] (aāœ : M) :
      opMulEquiv aāœ = op aāœ
      source
      šŸ“ coverage
      @[simp]
      theorem AddOpposite.opAddEquiv_symm_apply {M : Type u_1} [AddCommMonoid M] (aāœ : Mįµƒįµ’įµ–) :
      opAddEquiv.symm aāœ = unop aāœ
      source
      šŸ“ coverage
      @[simp]
      theorem MulOpposite.coe_opMulEquiv {M : Type u_1} [CommMonoid M] :
      ā‡‘opMulEquiv = op
      source
      šŸ“ coverage
      @[simp]
      theorem AddOpposite.coe_opAddEquiv {M : Type u_1} [AddCommMonoid M] :
      ā‡‘opAddEquiv = op
      source
      šŸ“ coverage
      @[simp]
      theorem MulOpposite.coe_symm_opMulEquiv {M : Type u_1} [CommMonoid M] :
      ā‡‘opMulEquiv.symm = unop
      source
      šŸ“ coverage
      @[simp]
      theorem AddOpposite.coe_symm_opAddEquiv {M : Type u_1} [AddCommMonoid M] :
      ā‡‘opAddEquiv.symm = unop
      source
      šŸ”ø coverage
      def MulOpposite.opAddEquiv {Ī± : Type u_2} [Add Ī±] :
      Ī± ā‰ƒ+ Ī±įµįµ’įµ–

      The function MulOpposite.op is an additive equivalence.

      Instances For
        source
        šŸ“ coverage
        @[simp]
        theorem MulOpposite.opAddEquiv_symm_apply {Ī± : Type u_2} [Add Ī±] :
        ā‡‘opAddEquiv.symm = unop
        source
        šŸ“ coverage
        @[simp]
        theorem MulOpposite.opAddEquiv_apply {Ī± : Type u_2} [Add Ī±] :
        ā‡‘opAddEquiv = op
        source
        šŸ“ coverage
        @[simp]
        theorem MulOpposite.opAddEquiv_toEquiv {Ī± : Type u_2} [Add Ī±] :
        ā†‘opAddEquiv = opEquiv
        source
        šŸ”ø coverage
        def AddOpposite.opMulEquiv {Ī± : Type u_2} [Mul Ī±] :
        Ī± ā‰ƒ* Ī±įµƒįµ’įµ–

        The function AddOpposite.op is a multiplicative equivalence.

        Instances For
          source
          šŸ“ coverage
          @[simp]
          theorem AddOpposite.opMulEquiv_symm_apply {Ī± : Type u_2} [Mul Ī±] :
          ā‡‘opMulEquiv.symm = unop
          source
          šŸ“ coverage
          @[simp]
          theorem AddOpposite.opMulEquiv_apply {Ī± : Type u_2} [Mul Ī±] :
          ā‡‘opMulEquiv = op
          source
          šŸ“ coverage
          @[simp]
          theorem AddOpposite.opMulEquiv_toEquiv {Ī± : Type u_2} [Mul Ī±] :
          ā†‘opMulEquiv = opEquiv
          source
          šŸ”ø coverage
          def MulEquiv.inv' (G : Type u_3) [DivisionMonoid G] :
          G ā‰ƒ* Gįµįµ’įµ–

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

          Instances For
            source
            šŸ”ø coverage
            def AddEquiv.neg' (G : Type u_3) [SubtractionMonoid G] :
            G ā‰ƒ+ Gįµƒįµ’įµ–

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

            Instances For
              source
              šŸ“ coverage
              @[simp]
              theorem MulEquiv.inv'_apply (G : Type u_3) [DivisionMonoid G] :
              ā‡‘(inv' G) = MulOpposite.op āˆ˜ Inv.inv
              source
              šŸ“ coverage
              @[simp]
              theorem AddEquiv.neg'_symm_apply (G : Type u_3) [SubtractionMonoid G] :
              ā‡‘(neg' G).symm = Neg.neg āˆ˜ AddOpposite.unop
              source
              šŸ“ coverage
              @[simp]
              theorem MulEquiv.inv'_symm_apply (G : Type u_3) [DivisionMonoid G] :
              ā‡‘(inv' G).symm = Inv.inv āˆ˜ MulOpposite.unop
              source
              šŸ“ coverage
              @[simp]
              theorem AddEquiv.neg'_apply (G : Type u_3) [SubtractionMonoid G] :
              ā‡‘(neg' G) = AddOpposite.op āˆ˜ Neg.neg
              source
              šŸ”ø coverage
              def MulHom.toOpposite {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ā†’ā‚™* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
              M ā†’ā‚™* Nįµįµ’įµ–

              A semigroup homomorphism f : M ā†’ā‚™* N such that f x commutes with f y for all x, y defines a semigroup homomorphism to Nįµįµ’įµ–.

              Instances For
                source
                šŸ”ø coverage
                def AddHom.toOpposite {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                M ā†’ā‚™+ Nįµƒįµ’įµ–

                An additive semigroup homomorphism f : AddHom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism to Sįµƒįµ’įµ–.

                Instances For
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem MulHom.toOpposite_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ā†’ā‚™* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                  ā‡‘(f.toOpposite hf) = MulOpposite.op āˆ˜ ā‡‘f
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem AddHom.toOpposite_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                  ā‡‘(f.toOpposite hf) = AddOpposite.op āˆ˜ ā‡‘f
                  source
                  šŸ”ø coverage
                  def MulHom.fromOpposite {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ā†’ā‚™* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                  Mįµįµ’įµ– ā†’ā‚™* N

                  A semigroup homomorphism f : M ā†’ā‚™* N such that f x commutes with f y for all x, y defines a semigroup homomorphism from Mįµįµ’įµ–.

                  Instances For
                    source
                    šŸ”ø coverage
                    def AddHom.fromOpposite {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                    Mįµƒįµ’įµ– ā†’ā‚™+ N

                    An additive semigroup homomorphism f : AddHom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism from Mįµƒįµ’įµ–.

                    Instances For
                      source
                      šŸ“ coverage
                      @[simp]
                      theorem AddHom.fromOpposite_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                      ā‡‘(f.fromOpposite hf) = ā‡‘f āˆ˜ AddOpposite.unop
                      source
                      šŸ“ coverage
                      @[simp]
                      theorem MulHom.fromOpposite_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ā†’ā‚™* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                      ā‡‘(f.fromOpposite hf) = ā‡‘f āˆ˜ MulOpposite.unop
                      source
                      šŸ”ø coverage
                      def MonoidHom.toOpposite {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : M ā†’* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                      M ā†’* Nįµįµ’įµ–

                      A monoid homomorphism f : M ā†’* N such that f x commutes with f y for all x, y defines a monoid homomorphism to Nįµįµ’įµ–.

                      Instances For
                        source
                        šŸ”ø coverage
                        def AddMonoidHom.toOpposite {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                        M ā†’+ Nįµƒįµ’įµ–

                        An additive monoid homomorphism f : M ā†’+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism to Sįµƒįµ’įµ–.

                        Instances For
                          source
                          šŸ“ coverage
                          @[simp]
                          theorem MonoidHom.toOpposite_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : M ā†’* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                          ā‡‘(f.toOpposite hf) = MulOpposite.op āˆ˜ ā‡‘f
                          source
                          šŸ“ coverage
                          @[simp]
                          theorem AddMonoidHom.toOpposite_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                          ā‡‘(f.toOpposite hf) = AddOpposite.op āˆ˜ ā‡‘f
                          source
                          šŸ”ø coverage
                          def MonoidHom.fromOpposite {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : M ā†’* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                          Mįµįµ’įµ– ā†’* N

                          A monoid homomorphism f : M ā†’* N such that f x commutes with f y for all x, y defines a monoid homomorphism from Mįµįµ’įµ–.

                          Instances For
                            source
                            šŸ”ø coverage
                            def AddMonoidHom.fromOpposite {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                            Mįµƒįµ’įµ– ā†’+ N

                            An additive monoid homomorphism f : M ā†’+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism from Mįµƒįµ’įµ–.

                            Instances For
                              source
                              šŸ“ coverage
                              @[simp]
                              theorem AddMonoidHom.fromOpposite_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (hf : āˆ€ (x y : M), AddCommute (f x) (f y)) :
                              ā‡‘(f.fromOpposite hf) = ā‡‘f āˆ˜ AddOpposite.unop
                              source
                              šŸ“ coverage
                              @[simp]
                              theorem MonoidHom.fromOpposite_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : M ā†’* N) (hf : āˆ€ (x y : M), Commute (f x) (f y)) :
                              ā‡‘(f.fromOpposite hf) = ā‡‘f āˆ˜ MulOpposite.unop
                              source
                              šŸ”ø coverage
                              def MulHom.op {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
                              (M ā†’ā‚™* N) ā‰ƒ (Mįµįµ’įµ– ā†’ā‚™* Nįµįµ’įµ–)

                              A semigroup homomorphism M ā†’ā‚™* N can equivalently be viewed as a semigroup homomorphism Mįµįµ’įµ– ā†’ā‚™* Nįµįµ’įµ–. This is the action of the (fully faithful) įµįµ’įµ–-functor on morphisms.

                              Instances For
                                source
                                šŸ”ø coverage
                                def AddHom.op {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
                                (M ā†’ā‚™+ N) ā‰ƒ (Mįµƒįµ’įµ– ā†’ā‚™+ Nįµƒįµ’įµ–)

                                An additive semigroup homomorphism AddHom M N can equivalently be viewed as an additive semigroup homomorphism AddHom Mįµƒįµ’įµ– Nįµƒįµ’įµ–. This is the action of the (fully faithful)įµƒįµ’įµ–-functor on morphisms.

                                Instances For
                                  source
                                  šŸ“ coverage
                                  @[simp]
                                  theorem AddHom.op_symm_apply_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : Mįµƒįµ’įµ– ā†’ā‚™+ Nįµƒįµ’įµ–) (aāœ : M) :
                                  (op.symm f) aāœ = (AddOpposite.unop āˆ˜ ā‡‘f āˆ˜ AddOpposite.op) aāœ
                                  source
                                  šŸ“ coverage
                                  @[simp]
                                  theorem MulHom.op_symm_apply_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : Mįµįµ’įµ– ā†’ā‚™* Nįµįµ’įµ–) (aāœ : M) :
                                  (op.symm f) aāœ = (MulOpposite.unop āˆ˜ ā‡‘f āˆ˜ MulOpposite.op) aāœ
                                  source
                                  šŸ“ coverage
                                  @[simp]
                                  theorem MulHom.op_apply_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ā†’ā‚™* N) (aāœ : Mįµįµ’įµ–) :
                                  (op f) aāœ = (MulOpposite.op āˆ˜ ā‡‘f āˆ˜ MulOpposite.unop) aāœ
                                  source
                                  šŸ“ coverage
                                  @[simp]
                                  theorem AddHom.op_apply_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (aāœ : Mįµƒįµ’įµ–) :
                                  (op f) aāœ = (AddOpposite.op āˆ˜ ā‡‘f āˆ˜ AddOpposite.unop) aāœ
                                  source
                                  šŸ”ø coverage
                                  def MulHom.unop {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
                                  (Mįµįµ’įµ– ā†’ā‚™* Nįµįµ’įµ–) ā‰ƒ (M ā†’ā‚™* N)

                                  The 'unopposite' of a semigroup homomorphism Mįµįµ’įµ– ā†’ā‚™* Nįµįµ’įµ–. Inverse to MulHom.op.

                                  Instances For
                                    source
                                    šŸ”ø coverage
                                    def AddHom.unop {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
                                    (Mįµƒįµ’įµ– ā†’ā‚™+ Nįµƒįµ’įµ–) ā‰ƒ (M ā†’ā‚™+ N)

                                    The 'unopposite' of an additive semigroup homomorphism Mįµƒįµ’įµ– ā†’ā‚™+ Nįµƒįµ’įµ–. Inverse to AddHom.op.

                                    Instances For
                                      source
                                      šŸ”ø coverage
                                      def AddHom.mulOp {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
                                      (M ā†’ā‚™+ N) ā‰ƒ (Mįµįµ’įµ– ā†’ā‚™+ Nįµįµ’įµ–)

                                      An additive semigroup homomorphism AddHom M N can equivalently be viewed as an additive homomorphism AddHom Mįµįµ’įµ– Nįµįµ’įµ–. This is the action of the (fully faithful) įµįµ’įµ–-functor on morphisms.

                                      Instances For
                                        source
                                        šŸ“ coverage
                                        @[simp]
                                        theorem AddHom.mulOp_apply_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M ā†’ā‚™+ N) (aāœ : Mįµįµ’įµ–) :
                                        (mulOp f) aāœ = (MulOpposite.op āˆ˜ ā‡‘f āˆ˜ MulOpposite.unop) aāœ
                                        source
                                        šŸ“ coverage
                                        @[simp]
                                        theorem AddHom.mulOp_symm_apply_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : Mįµįµ’įµ– ā†’ā‚™+ Nįµįµ’įµ–) (aāœ : M) :
                                        (mulOp.symm f) aāœ = (MulOpposite.unop āˆ˜ ā‡‘f āˆ˜ MulOpposite.op) aāœ
                                        source
                                        šŸ”ø coverage
                                        def AddHom.mulUnop {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] :
                                        (Ī±įµįµ’įµ– ā†’ā‚™+ Ī²įµįµ’įµ–) ā‰ƒ (Ī± ā†’ā‚™+ Ī²)

                                        The 'unopposite' of an additive semigroup hom Ī±įµįµ’įµ– ā†’+ Ī²įµįµ’įµ–. Inverse to AddHom.mul_op.

                                        Instances For
                                          source
                                          šŸ”ø coverage
                                          def MonoidHom.op {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                          (M ā†’* N) ā‰ƒ (Mįµįµ’įµ– ā†’* Nįµįµ’įµ–)

                                          A monoid homomorphism M ā†’* N can equivalently be viewed as a monoid homomorphism Mįµįµ’įµ– ā†’* Nįµįµ’įµ–. This is the action of the (fully faithful) įµįµ’įµ–-functor on morphisms.

                                          Instances For
                                            source
                                            šŸ”ø coverage
                                            def AddMonoidHom.op {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                            (M ā†’+ N) ā‰ƒ (Mįµƒįµ’įµ– ā†’+ Nįµƒįµ’įµ–)

                                            An additive monoid homomorphism M ā†’+ N can equivalently be viewed as an additive monoid homomorphism Mįµƒįµ’įµ– ā†’+ Nįµƒįµ’įµ–. This is the action of the (fully faithful) įµƒįµ’įµ–-functor on morphisms.

                                            Instances For
                                              source
                                              šŸ“ coverage
                                              @[simp]
                                              theorem MonoidHom.op_apply_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : M ā†’* N) (aāœ : Mįµįµ’įµ–) :
                                              (op f) aāœ = (MulOpposite.op āˆ˜ ā‡‘f āˆ˜ MulOpposite.unop) aāœ
                                              source
                                              šŸ“ coverage
                                              @[simp]
                                              theorem AddMonoidHom.op_apply_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (aāœ : Mįµƒįµ’įµ–) :
                                              (op f) aāœ = (AddOpposite.op āˆ˜ ā‡‘f āˆ˜ AddOpposite.unop) aāœ
                                              source
                                              šŸ“ coverage
                                              @[simp]
                                              theorem MonoidHom.op_symm_apply_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (f : Mįµįµ’įµ– ā†’* Nįµįµ’įµ–) (aāœ : M) :
                                              (op.symm f) aāœ = (MulOpposite.unop āˆ˜ ā‡‘f āˆ˜ MulOpposite.op) aāœ
                                              source
                                              šŸ“ coverage
                                              @[simp]
                                              theorem AddMonoidHom.op_symm_apply_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : Mįµƒįµ’įµ– ā†’+ Nįµƒįµ’įµ–) (aāœ : M) :
                                              (op.symm f) aāœ = (AddOpposite.unop āˆ˜ ā‡‘f āˆ˜ AddOpposite.op) aāœ
                                              source
                                              šŸ”ø coverage
                                              def MonoidHom.unop {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                              (Mįµįµ’įµ– ā†’* Nįµįµ’įµ–) ā‰ƒ (M ā†’* N)

                                              The 'unopposite' of a monoid homomorphism Mįµįµ’įµ– ā†’* Nįµįµ’įµ–. Inverse to MonoidHom.op.

                                              Instances For
                                                source
                                                šŸ”ø coverage
                                                def AddMonoidHom.unop {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                                (Mįµƒįµ’įµ– ā†’+ Nįµƒįµ’įµ–) ā‰ƒ (M ā†’+ N)

                                                The 'unopposite' of an additive monoid homomorphism Mįµƒįµ’įµ– ā†’+ Nįµƒįµ’įµ–. Inverse to AddMonoidHom.op.

                                                Instances For
                                                  source
                                                  šŸ”ø coverage
                                                  def MulEquiv.opOp (M : Type u_3) [Mul M] :
                                                  M ā‰ƒ* Mįµįµ’įµ–įµįµ’įµ–

                                                  A monoid is isomorphic to the opposite of its opposite.

                                                  Instances For
                                                    source
                                                    šŸ”ø coverage
                                                    def AddEquiv.opOp (M : Type u_3) [Add M] :
                                                    M ā‰ƒ+ Mįµƒįµ’įµ–įµƒįµ’įµ–

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

                                                    Instances For
                                                      source
                                                      šŸ“ coverage
                                                      @[simp]
                                                      theorem AddEquiv.opOp_apply (M : Type u_3) [Add M] (aāœ : M) :
                                                      (opOp M) aāœ = AddOpposite.op (AddOpposite.op aāœ)
                                                      source
                                                      šŸ“ coverage
                                                      @[simp]
                                                      theorem MulEquiv.opOp_apply (M : Type u_3) [Mul M] (aāœ : M) :
                                                      (opOp M) aāœ = MulOpposite.op (MulOpposite.op aāœ)
                                                      source
                                                      šŸ“ coverage
                                                      @[simp]
                                                      theorem AddEquiv.opOp_symm_apply (M : Type u_3) [Add M] (aāœ : Mįµƒįµ’įµ–įµƒįµ’įµ–) :
                                                      (opOp M).symm aāœ = AddOpposite.unop (AddOpposite.unop aāœ)
                                                      source
                                                      šŸ“ coverage
                                                      @[simp]
                                                      theorem MulEquiv.opOp_symm_apply (M : Type u_3) [Mul M] (aāœ : Mįµįµ’įµ–įµįµ’įµ–) :
                                                      (opOp M).symm aāœ = MulOpposite.unop (MulOpposite.unop aāœ)
                                                      source
                                                      šŸ”ø coverage
                                                      def AddMonoidHom.mulOp {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                                      (M ā†’+ N) ā‰ƒ (Mįµįµ’įµ– ā†’+ Nįµįµ’įµ–)

                                                      An additive homomorphism M ā†’+ N can equivalently be viewed as an additive homomorphism Mįµįµ’įµ– ā†’+ Nįµįµ’įµ–. This is the action of the (fully faithful) įµįµ’įµ–-functor on morphisms.

                                                      Instances For
                                                        source
                                                        šŸ“ coverage
                                                        @[simp]
                                                        theorem AddMonoidHom.mulOp_apply_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : M ā†’+ N) (aāœ : Mįµįµ’įµ–) :
                                                        (mulOp f) aāœ = (MulOpposite.op āˆ˜ ā‡‘f āˆ˜ MulOpposite.unop) aāœ
                                                        source
                                                        šŸ“ coverage
                                                        @[simp]
                                                        theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (f : Mįµįµ’įµ– ā†’+ Nįµįµ’įµ–) (aāœ : M) :
                                                        (mulOp.symm f) aāœ = (MulOpposite.unop āˆ˜ ā‡‘f āˆ˜ MulOpposite.op) aāœ
                                                        source
                                                        šŸ”ø coverage
                                                        def AddMonoidHom.mulUnop {Ī± : Type u_3} {Ī² : Type u_4} [AddZeroClass Ī±] [AddZeroClass Ī²] :
                                                        (Ī±įµįµ’įµ– ā†’+ Ī²įµįµ’įµ–) ā‰ƒ (Ī± ā†’+ Ī²)

                                                        The 'unopposite' of an additive monoid hom Ī±įµįµ’įµ– ā†’+ Ī²įµįµ’įµ–. Inverse to AddMonoidHom.mul_op.

                                                        Instances For
                                                          source
                                                          šŸ”ø coverage
                                                          def AddEquiv.mulOp {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] :
                                                          Ī± ā‰ƒ+ Ī² ā‰ƒ (Ī±įµįµ’įµ– ā‰ƒ+ Ī²įµįµ’įµ–)

                                                          An iso Ī± ā‰ƒ+ Ī² can equivalently be viewed as an iso Ī±įµįµ’įµ– ā‰ƒ+ Ī²įµįµ’įµ–.

                                                          Instances For
                                                            source
                                                            šŸ“ coverage
                                                            @[simp]
                                                            theorem AddEquiv.mulOp_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī± ā‰ƒ+ Ī²) :
                                                            mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)
                                                            source
                                                            šŸ“ coverage
                                                            @[simp]
                                                            theorem AddEquiv.mulOp_symm_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī±įµįµ’įµ– ā‰ƒ+ Ī²įµįµ’įµ–) :
                                                            mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)
                                                            source
                                                            šŸ”ø coverage
                                                            def AddEquiv.mulUnop {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] :
                                                            Ī±įµįµ’įµ– ā‰ƒ+ Ī²įµįµ’įµ– ā‰ƒ (Ī± ā‰ƒ+ Ī²)

                                                            The 'unopposite' of an iso Ī±įµįµ’įµ– ā‰ƒ+ Ī²įµįµ’įµ–. Inverse to AddEquiv.mul_op.

                                                            Instances For
                                                              source
                                                              šŸ”ø coverage
                                                              def MulEquiv.op {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] :
                                                              Ī± ā‰ƒ* Ī² ā‰ƒ (Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ–)

                                                              An iso Ī± ā‰ƒ* Ī² can equivalently be viewed as an iso Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ–.

                                                              Instances For
                                                                source
                                                                šŸ”ø coverage
                                                                def AddEquiv.op {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] :
                                                                Ī± ā‰ƒ+ Ī² ā‰ƒ (Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ–)

                                                                An iso Ī± ā‰ƒ+ Ī² can equivalently be viewed as an iso Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ–.

                                                                Instances For
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem AddEquiv.op_apply_symm_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī± ā‰ƒ+ Ī²) (aāœ : Ī²įµƒįµ’įµ–) :
                                                                  (op f).symm aāœ = (AddOpposite.op āˆ˜ ā‡‘f.symm āˆ˜ AddOpposite.unop) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem MulEquiv.op_apply_apply {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] (f : Ī± ā‰ƒ* Ī²) (aāœ : Ī±įµįµ’įµ–) :
                                                                  (op f) aāœ = (MulOpposite.op āˆ˜ ā‡‘f āˆ˜ MulOpposite.unop) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem AddEquiv.op_apply_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī± ā‰ƒ+ Ī²) (aāœ : Ī±įµƒįµ’įµ–) :
                                                                  (op f) aāœ = (AddOpposite.op āˆ˜ ā‡‘f āˆ˜ AddOpposite.unop) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem AddEquiv.op_symm_apply_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ–) (aāœ : Ī±) :
                                                                  (op.symm f) aāœ = (AddOpposite.unop āˆ˜ ā‡‘f āˆ˜ AddOpposite.op) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem MulEquiv.op_apply_symm_apply {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] (f : Ī± ā‰ƒ* Ī²) (aāœ : Ī²įµįµ’įµ–) :
                                                                  (op f).symm aāœ = (MulOpposite.op āˆ˜ ā‡‘f.symm āˆ˜ MulOpposite.unop) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem AddEquiv.op_symm_apply_symm_apply {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] (f : Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ–) (aāœ : Ī²) :
                                                                  (op.symm f).symm aāœ = (AddOpposite.unop āˆ˜ ā‡‘f.symm āˆ˜ AddOpposite.op) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem MulEquiv.op_symm_apply_apply {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] (f : Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ–) (aāœ : Ī±) :
                                                                  (op.symm f) aāœ = (MulOpposite.unop āˆ˜ ā‡‘f āˆ˜ MulOpposite.op) aāœ
                                                                  source
                                                                  šŸ“ coverage
                                                                  @[simp]
                                                                  theorem MulEquiv.op_symm_apply_symm_apply {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] (f : Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ–) (aāœ : Ī²) :
                                                                  (op.symm f).symm aāœ = (MulOpposite.unop āˆ˜ ā‡‘f.symm āˆ˜ MulOpposite.op) aāœ
                                                                  source
                                                                  šŸ”ø coverage
                                                                  def MulEquiv.unop {Ī± : Type u_3} {Ī² : Type u_4} [Mul Ī±] [Mul Ī²] :
                                                                  Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ– ā‰ƒ (Ī± ā‰ƒ* Ī²)

                                                                  The 'unopposite' of an iso Ī±įµįµ’įµ– ā‰ƒ* Ī²įµįµ’įµ–. Inverse to MulEquiv.op.

                                                                  Instances For
                                                                    source
                                                                    šŸ”ø coverage
                                                                    def AddEquiv.unop {Ī± : Type u_3} {Ī² : Type u_4} [Add Ī±] [Add Ī²] :
                                                                    Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ– ā‰ƒ (Ī± ā‰ƒ+ Ī²)

                                                                    The 'unopposite' of an iso Ī±įµƒįµ’įµ– ā‰ƒ+ Ī²įµƒįµ’įµ–. Inverse to AddEquiv.op.

                                                                    Instances For
                                                                      source
                                                                      theorem AddMonoidHom.mul_op_ext {Ī± : Type u_3} {Ī² : Type u_4} [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'.

                                                                      source
                                                                      šŸ“ coverage
                                                                      theorem AddMonoidHom.mul_op_ext_iff {Ī± : Type u_3} {Ī² : Type u_4} [AddZeroClass Ī±] [AddZeroClass Ī²] {f g : Ī±įµįµ’įµ– ā†’+ Ī²} :
                                                                      f = g ā†” f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom