Documentation

Mathlib.Algebra.Group.Equiv.Basic

Multiplicative and additive equivs #

This file contains basic results on MulEquiv and AddEquiv.

Tags #

Equiv, MulEquiv, AddEquiv

theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
def MulEquiv.ofUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Mul M] [Mul N] :
M ≃* N

The MulEquiv between two monoids with a unique element.

Equations
Instances For
    def AddEquiv.ofUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Add M] [Add N] :
    M ≃+ N

    The AddEquiv between two AddMonoids with a unique element.

    Equations
    Instances For
      instance MulEquiv.instUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Mul M] [Mul N] :
      Unique (M ≃* N)

      There is a unique monoid homomorphism between two monoids with a unique element.

      Equations
      instance AddEquiv.instUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Add M] [Add N] :
      Unique (M ≃+ N)

      There is a unique additive monoid homomorphism between two additive monoids with a unique element.

      Equations

      Monoids #

      def MulEquiv.arrowCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) :
      (MP) ≃* (NQ)

      A multiplicative analogue of Equiv.arrowCongr, where the equivalence between the targets is multiplicative.

      Equations
      • MulEquiv.arrowCongr f g = { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => g.symm (k (f m)), left_inv := , right_inv := , map_mul' := }
      Instances For
        def AddEquiv.arrowCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) :
        (MP) ≃+ (NQ)

        An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

        Equations
        • AddEquiv.arrowCongr f g = { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => g.symm (k (f m)), left_inv := , right_inv := , map_add' := }
        Instances For
          @[simp]
          theorem AddEquiv.arrowCongr_apply {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (n : N) :
          (arrowCongr f g) h n = g (h (f.symm n))
          @[simp]
          theorem MulEquiv.arrowCongr_apply {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) (h : MP) (n : N) :
          (arrowCongr f g) h n = g (h (f.symm n))
          def MulEquiv.monoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) :
          (M₁ →* N) (M₂ →* N)

          The equivalence (M₁ →* N) ≃ (M₂ →* N) obtained by postcomposition with a multiplicative equivalence e : M₁ ≃* M₂.

          Equations
          Instances For
            def AddEquiv.addMonoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) :
            (M₁ →+ N) (M₂ →+ N)

            The equivalence (M₁ →+ N) ≃ (M₂ →+ N) obtained by postcomposition with an additive equivalence e : M₁ ≃+ M₂.

            Equations
            Instances For
              @[simp]
              theorem MulEquiv.monoidHomCongrLeftEquiv_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) (f : M₁ →* N) :
              @[simp]
              theorem AddEquiv.addMonoidHomCongrLeftEquiv_symm_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) (f : M₂ →+ N) :
              @[simp]
              theorem MulEquiv.monoidHomCongrLeftEquiv_symm_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) (f : M₂ →* N) :
              @[simp]
              theorem AddEquiv.addMonoidHomCongrLeftEquiv_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N) :
              def MulEquiv.monoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) :
              (M →* N₁) (M →* N₂)

              The equivalence (M →* N₁) ≃ (M →* N₂) obtained by postcomposition with a multiplicative equivalence e : N₁ ≃* N₂.

              Equations
              Instances For
                def AddEquiv.addMonoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) :
                (M →+ N₁) (M →+ N₂)

                The equivalence (M →+ N₁) ≃ (M →+ N₂) obtained by postcomposition with an additive equivalence e : N₁ ≃+ N₂.

                Equations
                Instances For
                  @[simp]
                  theorem MulEquiv.monoidHomCongrRightEquiv_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₁) :
                  @[simp]
                  theorem MulEquiv.monoidHomCongrRightEquiv_symm_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₂) :
                  @[simp]
                  theorem AddEquiv.addMonoidHomCongrRightEquiv_symm_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₂) :
                  @[simp]
                  theorem AddEquiv.addMonoidHomCongrRightEquiv_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁) :
                  @[simp]
                  theorem MulEquiv.symm_monoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) :
                  @[simp]
                  theorem MulEquiv.symm_monoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) :
                  @[simp]
                  @[simp]
                  theorem MulEquiv.monoidHomCongrLeftEquiv_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [MulOneClass M₃] [Monoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃) :
                  @[simp]
                  theorem AddEquiv.addMonoidHomCongrLeftEquiv_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddZeroClass M₃] [AddMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃) :
                  @[simp]
                  theorem MulEquiv.monoidHomCongrRightEquiv_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [MulOneClass M] [Monoid N₁] [Monoid N₂] [Monoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃) :
                  @[simp]
                  theorem AddEquiv.addMonoidHomCongrRightEquiv_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] [AddMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃) :
                  def MulEquiv.monoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) :
                  (M₁ →* N) ≃* (M₂ →* N)

                  The isomorphism (M₁ →* N) ≃* (M₂ →* N) obtained by postcomposition with a multiplicative equivalence e : M₁ ≃* M₂.

                  Equations
                  Instances For
                    def AddEquiv.addMonoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) :
                    (M₁ →+ N) ≃+ (M₂ →+ N)

                    The isomorphism (M₁ →+ N) ≃+ (M₂ →+ N) obtained by postcomposition with an additive equivalence e : M₁ ≃+ M₂.

                    Equations
                    Instances For
                      @[simp]
                      theorem AddEquiv.addMonoidHomCongrLeft_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N) :
                      @[simp]
                      theorem MulEquiv.monoidHomCongrLeft_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) (f : M₁ →* N) :
                      def MulEquiv.monoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) :
                      (M →* N₁) ≃* (M →* N₂)

                      The isomorphism (M →* N₁) ≃* (M →* N₂) obtained by postcomposition with a multiplicative equivalence e : N₁ ≃* N₂.

                      Equations
                      Instances For
                        def AddEquiv.addMonoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) :
                        (M →+ N₁) ≃+ (M →+ N₂)

                        The isomorphism (M →+ N₁) ≃+ (M →+ N₂) obtained by postcomposition with an additive equivalence e : N₁ ≃+ N₂.

                        Equations
                        Instances For
                          @[simp]
                          theorem AddEquiv.addMonoidHomCongrRight_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁) :
                          e.addMonoidHomCongrRight hmn = (↑e).comp hmn
                          @[simp]
                          theorem MulEquiv.monoidHomCongrRight_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₁) :
                          e.monoidHomCongrRight hmn = (↑e).comp hmn
                          @[simp]
                          theorem MulEquiv.symm_monoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) :
                          @[simp]
                          theorem AddEquiv.symm_addMonoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) :
                          @[simp]
                          theorem MulEquiv.symm_monoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) :
                          @[simp]
                          theorem AddEquiv.symm_addMonoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) :
                          @[simp]
                          theorem MulEquiv.monoidHomCongrLeft_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [MulOneClass M₃] [CommMonoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃) :
                          @[simp]
                          theorem AddEquiv.addMonoidHomCongrLeft_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddZeroClass M₃] [AddCommMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃) :
                          @[simp]
                          theorem MulEquiv.monoidHomCongrRight_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] [CommMonoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃) :
                          @[simp]
                          theorem AddEquiv.addMonoidHomCongrRight_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃) :
                          @[deprecated MulEquiv.monoidHomCongrLeft (since := "2025-08-12")]
                          def MulEquiv.monoidHomCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) :
                          (M →* P) ≃* (N →* Q)

                          A multiplicative analogue of Equiv.arrowCongr, for multiplicative maps from a monoid to a commutative monoid.

                          Equations
                          Instances For
                            @[deprecated MulEquiv.monoidHomCongrLeft (since := "2025-08-12")]
                            def AddEquiv.addMonoidHomCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) :
                            (M →+ P) ≃+ (N →+ Q)

                            An additive analogue of Equiv.arrowCongr, for additive maps from an additive monoid to a commutative additive monoid.

                            Equations
                            Instances For
                              def MulEquiv.piCongrRight {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
                              ((j : η) → Ms j) ≃* ((j : η) → Ns j)

                              A family of multiplicative equivalences Π j, (Ms j ≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j.

                              This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def AddEquiv.piCongrRight {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
                                ((j : η) → Ms j) ≃+ ((j : η) → Ns j)

                                A family of additive equivalences Π j, (Ms j ≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j.

                                This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem AddEquiv.piCongrRight_apply {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
                                  (piCongrRight es) x j = (es j) (x j)
                                  @[simp]
                                  theorem MulEquiv.piCongrRight_apply {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
                                  (piCongrRight es) x j = (es j) (x j)
                                  @[simp]
                                  theorem MulEquiv.piCongrRight_refl {η : Type u_16} {Ms : ηType u_17} [(j : η) → Mul (Ms j)] :
                                  (piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)
                                  @[simp]
                                  theorem AddEquiv.piCongrRight_refl {η : Type u_16} {Ms : ηType u_17} [(j : η) → Add (Ms j)] :
                                  (piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)
                                  @[simp]
                                  theorem MulEquiv.piCongrRight_symm {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
                                  (piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm
                                  @[simp]
                                  theorem AddEquiv.piCongrRight_symm {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
                                  (piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm
                                  @[simp]
                                  theorem MulEquiv.piCongrRight_trans {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} {Ps : ηType u_19} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
                                  (piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)
                                  @[simp]
                                  theorem AddEquiv.piCongrRight_trans {η : Type u_16} {Ms : ηType u_17} {Ns : ηType u_18} {Ps : ηType u_19} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
                                  (piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)
                                  def MulEquiv.piUnique {ι : Type u_16} (M : ιType u_17) [(j : ι) → Mul (M j)] [Unique ι] :
                                  ((j : ι) → M j) ≃* M default

                                  A family indexed by a type with a unique element is MulEquiv to the element at the single index.

                                  Equations
                                  Instances For
                                    def AddEquiv.piUnique {ι : Type u_16} (M : ιType u_17) [(j : ι) → Add (M j)] [Unique ι] :
                                    ((j : ι) → M j) ≃+ M default

                                    A family indexed by a type with a unique element is AddEquiv to the element at the single index.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem MulEquiv.piUnique_symm_apply {ι : Type u_16} (M : ιType u_17) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) :
                                      @[simp]
                                      theorem AddEquiv.piUnique_symm_apply {ι : Type u_16} (M : ιType u_17) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) :
                                      @[simp]
                                      theorem AddEquiv.piUnique_apply {ι : Type u_16} (M : ιType u_17) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) :
                                      @[simp]
                                      theorem MulEquiv.piUnique_apply {ι : Type u_16} (M : ιType u_17) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) :
                                      @[deprecated MulEquiv.monoidHomCongrLeftEquiv (since := "2025-08-12")]
                                      def MonoidHom.precompEquiv {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] :
                                      (β →* γ) (α →* γ)

                                      The equivalence (β →* γ) ≃ (α →* γ) obtained by precomposition with a multiplicative equivalence e : α ≃* β.

                                      Equations
                                      Instances For
                                        @[deprecated MulEquiv.monoidHomCongrLeftEquiv (since := "2025-08-12")]
                                        def AddMonoidHom.precompEquiv {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] :
                                        (β →+ γ) (α →+ γ)

                                        The equivalence (β →+ γ) ≃ (α →+ γ) obtained by precomposition with an additive equivalence e : α ≃+ β.

                                        Equations
                                        Instances For
                                          theorem MonoidHom.precompEquiv_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (f : β →* γ) :
                                          (precompEquiv e γ) f = f.comp e
                                          theorem AddMonoidHom.precompEquiv_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (f : β →+ γ) :
                                          (precompEquiv e γ) f = f.comp e
                                          theorem MonoidHom.precompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (g : α →* γ) :
                                          (precompEquiv e γ).symm g = g.comp e.symm
                                          theorem AddMonoidHom.precompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (g : α →+ γ) :
                                          (precompEquiv e γ).symm g = g.comp e.symm
                                          @[deprecated MulEquiv.monoidHomCongrRightEquiv (since := "2025-08-12")]
                                          def MonoidHom.postcompEquiv {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] :
                                          (γ →* α) (γ →* β)

                                          The equivalence (γ →* α) ≃ (γ →* β) obtained by postcomposition with a multiplicative equivalence e : α ≃* β.

                                          Equations
                                          Instances For
                                            @[deprecated MulEquiv.monoidHomCongrRightEquiv (since := "2025-08-12")]
                                            def AddMonoidHom.postcompEquiv {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] :
                                            (γ →+ α) (γ →+ β)

                                            The equivalence (γ →+ α) ≃ (γ →+ β) obtained by postcomposition with an additive equivalence e : α ≃+ β.

                                            Equations
                                            Instances For
                                              theorem AddMonoidHom.postcompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (g : γ →+ β) :
                                              theorem MonoidHom.postcompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (g : γ →* β) :
                                              theorem MonoidHom.postcompEquiv_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (f : γ →* α) :
                                              theorem AddMonoidHom.postcompEquiv_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (f : γ →+ α) :
                                              def Equiv.inv (G : Type u_14) [InvolutiveInv G] :

                                              Inversion on a Group or GroupWithZero is a permutation of the underlying type.

                                              Equations
                                              Instances For
                                                def Equiv.neg (G : Type u_14) [InvolutiveNeg G] :

                                                Negation on an AddGroup is a permutation of the underlying type.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Equiv.neg_apply (G : Type u_14) [InvolutiveNeg G] :
                                                  @[simp]
                                                  theorem Equiv.inv_apply (G : Type u_14) [InvolutiveInv G] :
                                                  @[simp]
                                                  @[simp]