Documentation

Mathlib.Algebra.Group.Equiv.Basic

Multiplicative and additive equivs #

In this file we define two extensions of Equiv called AddEquiv and MulEquiv, which are datatypes representing isomorphisms of AddMonoids/AddGroups and Monoids/Groups.

Notations #

The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.

Tags #

Equiv, MulEquiv, AddEquiv

theorem ZeroHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : Function.LeftInverse g f) :
g 0 = 0
def ZeroHom.inverse {M : Type u_6} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : Function.LeftInverse g f) :

Make a ZeroHom inverse from the bijective inverse of a ZeroHom

Equations
  • f.inverse g h₁ = { toFun := g, map_zero' := }
Instances For
    @[simp]
    theorem OneHom.inverse_apply {M : Type u_6} {N : Type u_7} [One M] [One N] (f : OneHom M N) (g : NM) (h₁ : Function.LeftInverse g f) :
    ∀ (a : N), (f.inverse g h₁) a = g a
    @[simp]
    theorem ZeroHom.inverse_apply {M : Type u_6} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : Function.LeftInverse g f) :
    ∀ (a : N), (f.inverse g h₁) a = g a
    def OneHom.inverse {M : Type u_6} {N : Type u_7} [One M] [One N] (f : OneHom M N) (g : NM) (h₁ : Function.LeftInverse g f) :
    OneHom N M

    Makes a OneHom inverse from the bijective inverse of a OneHom

    Equations
    • f.inverse g h₁ = { toFun := g, map_one' := }
    Instances For
      def AddHom.inverse {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
      AddHom N M

      Makes an additive inverse from a bijection which preserves addition.

      Equations
      • f.inverse g h₁ h₂ = { toFun := g, map_add' := }
      Instances For
        theorem AddHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (x : N) (y : N) :
        g (x + y) = g x + g y
        @[simp]
        theorem AddHom.inverse_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
        ∀ (a : N), (f.inverse g h₁ h₂) a = g a
        @[simp]
        theorem MulHom.inverse_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
        ∀ (a : N), (f.inverse g h₁ h₂) a = g a
        def MulHom.inverse {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

        Makes a multiplicative inverse from a bijection which preserves multiplication.

        Equations
        • f.inverse g h₁ h₂ = { toFun := g, map_mul' := }
        Instances For
          theorem AddMonoidHom.inverse.proof_3 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) :
          ((↑f).inverse g h₁).toFun 0 = 0
          def AddMonoidHom.inverse {A : Type u_12} {B : Type u_13} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
          B →+ A

          The inverse of a bijective AddMonoidHom is an AddMonoidHom.

          Equations
          • f.inverse g h₁ h₂ = { toFun := g, map_zero' := , map_add' := }
          Instances For
            theorem AddMonoidHom.inverse.proof_4 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (x : B) (y : B) :
            ((↑f).inverse g h₁ h₂).toFun (x + y) = ((↑f).inverse g h₁ h₂).toFun x + ((↑f).inverse g h₁ h₂).toFun y
            theorem AddMonoidHom.inverse.proof_2 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] :
            AddHomClass (A →+ B) A B
            theorem AddMonoidHom.inverse.proof_1 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] :
            ZeroHomClass (A →+ B) A B
            @[simp]
            theorem MonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [Monoid A] [Monoid B] (f : A →* B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
            ∀ (a : B), (f.inverse g h₁ h₂) a = g a
            @[simp]
            theorem AddMonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
            ∀ (a : B), (f.inverse g h₁ h₂) a = g a
            def MonoidHom.inverse {A : Type u_12} {B : Type u_13} [Monoid A] [Monoid B] (f : A →* B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
            B →* A

            The inverse of a bijective MonoidHom is a MonoidHom.

            Equations
            • f.inverse g h₁ h₂ = { toFun := g, map_one' := , map_mul' := }
            Instances For
              structure AddEquiv (A : Type u_12) (B : Type u_13) [Add A] [Add B] extends Equiv :
              Type (max u_12 u_13)

              AddEquiv α β is the type of an equiv α ≃ β which preserves addition.

              • toFun : AB
              • invFun : BA
              • left_inv : Function.LeftInverse self.invFun self.toFun
              • right_inv : Function.RightInverse self.invFun self.toFun
              • map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y

                The proposition that the function preserves addition

              Instances For
                class AddEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Add A] [Add B] [EquivLike F A B] :

                AddEquivClass F A B states that F is a type of addition-preserving morphisms. You should extend this class when you extend AddEquiv.

                • map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b

                  Preserves addition.

                Instances
                  theorem AddEquivClass.map_add {F : Type u_12} {A : outParam (Type u_13)} {B : outParam (Type u_14)} :
                  ∀ {inst : Add A} {inst_1 : Add B} {inst_2 : EquivLike F A B} [self : AddEquivClass F A B] (f : F) (a b : A), f (a + b) = f a + f b

                  Preserves addition.

                  @[reducible]
                  abbrev AddEquiv.toAddHom {A : Type u_12} {B : Type u_13} [Add A] [Add B] (self : A ≃+ B) :
                  AddHom A B

                  The AddHom underlying an AddEquiv.

                  Equations
                  • self.toAddHom = { toFun := self.toFun, map_add' := }
                  Instances For
                    structure MulEquiv (M : Type u_12) (N : Type u_13) [Mul M] [Mul N] extends Equiv :
                    Type (max u_12 u_13)

                    MulEquiv α β is the type of an equiv α ≃ β which preserves multiplication.

                    • toFun : MN
                    • invFun : NM
                    • left_inv : Function.LeftInverse self.invFun self.toFun
                    • right_inv : Function.RightInverse self.invFun self.toFun
                    • map_mul' : ∀ (x y : M), self.toFun (x * y) = self.toFun x * self.toFun y

                      The proposition that the function preserves multiplication

                    Instances For
                      @[reducible]
                      abbrev MulEquiv.toMulHom {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (self : M ≃* N) :

                      The MulHom underlying a MulEquiv.

                      Equations
                      • self.toMulHom = { toFun := self.toFun, map_mul' := }
                      Instances For
                        class MulEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Mul A] [Mul B] [EquivLike F A B] :

                        MulEquivClass F A B states that F is a type of multiplication-preserving morphisms. You should extend this class when you extend MulEquiv.

                        • map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b

                          Preserves multiplication.

                        Instances
                          theorem MulEquivClass.map_mul {F : Type u_12} {A : outParam (Type u_13)} {B : outParam (Type u_14)} :
                          ∀ {inst : Mul A} {inst_1 : Mul B} {inst_2 : EquivLike F A B} [self : MulEquivClass F A B] (f : F) (a b : A), f (a * b) = f a * f b

                          Preserves multiplication.

                          @[instance 100]
                          instance AddEquivClass.instAddHomClass {M : Type u_6} {N : Type u_7} (F : Type u_12) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] :
                          Equations
                          • =
                          @[instance 100]
                          instance MulEquivClass.instMulHomClass {M : Type u_6} {N : Type u_7} (F : Type u_12) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] :
                          Equations
                          • =
                          @[instance 100]
                          instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [EquivLike F M N] [AddZeroClass M] [AddZeroClass N] [AddEquivClass F M N] :
                          Equations
                          • =
                          @[instance 100]
                          instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [EquivLike F M N] [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
                          Equations
                          • =
                          @[simp]
                          theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [AddZeroClass M] [AddZeroClass N] [EquivLike F M N] [AddEquivClass F M N] (h : F) {x : M} :
                          h x = 0 x = 0
                          @[simp]
                          theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [MulOneClass M] [MulOneClass N] [EquivLike F M N] [MulEquivClass F M N] (h : F) {x : M} :
                          h x = 1 x = 1
                          theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [AddZeroClass M] [AddZeroClass N] [EquivLike F M N] [AddEquivClass F M N] (h : F) {x : M} :
                          h x 0 x 0
                          theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [MulOneClass M] [MulOneClass N] [EquivLike F M N] [MulEquivClass F M N] (h : F) {x : M} :
                          h x 1 x 1
                          def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] (f : F) :
                          α ≃+ β

                          Turn an element of a type F satisfying AddEquivClass F α β into an actual AddEquiv. This is declared as the default coercion from F to α ≃+ β.

                          Equations
                          • f = { toEquiv := f, map_add' := }
                          Instances For
                            def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] (f : F) :
                            α ≃* β

                            Turn an element of a type F satisfying MulEquivClass F α β into an actual MulEquiv. This is declared as the default coercion from F to α ≃* β.

                            Equations
                            • f = { toEquiv := f, map_mul' := }
                            Instances For
                              instance instCoeTCAddEquivOfAddEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
                              CoeTC F (α ≃+ β)

                              Any type satisfying AddEquivClass can be cast into AddEquiv via AddEquivClass.toAddEquiv.

                              Equations
                              • instCoeTCAddEquivOfAddEquivClass = { coe := AddEquivClass.toAddEquiv }
                              instance instCoeTCMulEquivOfMulEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
                              CoeTC F (α ≃* β)

                              Any type satisfying MulEquivClass can be cast into MulEquiv via MulEquivClass.toMulEquiv.

                              Equations
                              • instCoeTCMulEquivOfMulEquivClass = { coe := MulEquivClass.toMulEquiv }
                              theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
                              Function.Injective AddEquivClass.toAddEquiv
                              theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
                              Function.Injective MulEquivClass.toMulEquiv
                              instance AddEquiv.instEquivLike {M : Type u_6} {N : Type u_7} [Add M] [Add N] :
                              EquivLike (M ≃+ N) M N
                              Equations
                              • AddEquiv.instEquivLike = { coe := fun (f : M ≃+ N) => f.toFun, inv := fun (f : M ≃+ N) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                              theorem AddEquiv.instEquivLike.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) :
                              Function.RightInverse f.invFun f.toFun
                              theorem AddEquiv.instEquivLike.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) :
                              Function.LeftInverse f.invFun f.toFun
                              theorem AddEquiv.instEquivLike.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) (g : M ≃+ N) (h₁ : (fun (f : M ≃+ N) => f.toFun) f = (fun (f : M ≃+ N) => f.toFun) g) (h₂ : (fun (f : M ≃+ N) => f.invFun) f = (fun (f : M ≃+ N) => f.invFun) g) :
                              f = g
                              instance MulEquiv.instEquivLike {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
                              EquivLike (M ≃* N) M N
                              Equations
                              • MulEquiv.instEquivLike = { coe := fun (f : M ≃* N) => f.toFun, inv := fun (f : M ≃* N) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                              instance AddEquiv.instCoeFunForall {M : Type u_6} {N : Type u_7} [Add M] [Add N] :
                              CoeFun (M ≃+ N) fun (x : M ≃+ N) => MN
                              Equations
                              • AddEquiv.instCoeFunForall = { coe := fun (f : M ≃+ N) => f }
                              instance MulEquiv.instCoeFunForall {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
                              CoeFun (M ≃* N) fun (x : M ≃* N) => MN
                              Equations
                              • MulEquiv.instCoeFunForall = { coe := fun (f : M ≃* N) => f }
                              instance AddEquiv.instAddEquivClass {M : Type u_6} {N : Type u_7} [Add M] [Add N] :
                              Equations
                              • =
                              instance MulEquiv.instMulEquivClass {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
                              Equations
                              • =
                              theorem AddEquiv.ext {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {g : M ≃+ N} (h : ∀ (x : M), f x = g x) :
                              f = g

                              Two additive isomorphisms agree if they are defined by the same underlying function.

                              theorem AddEquiv.ext_iff {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {g : M ≃+ N} :
                              f = g ∀ (x : M), f x = g x
                              theorem MulEquiv.ext_iff {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} :
                              f = g ∀ (x : M), f x = g x
                              theorem MulEquiv.ext {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} (h : ∀ (x : M), f x = g x) :
                              f = g

                              Two multiplicative isomorphisms agree if they are defined by the same underlying function.

                              theorem AddEquiv.congr_arg {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {x : M} {x' : M} :
                              x = x'f x = f x'
                              theorem MulEquiv.congr_arg {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {x : M} {x' : M} :
                              x = x'f x = f x'
                              theorem AddEquiv.congr_fun {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {g : M ≃+ N} (h : f = g) (x : M) :
                              f x = g x
                              theorem MulEquiv.congr_fun {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} (h : f = g) (x : M) :
                              f x = g x
                              @[simp]
                              theorem AddEquiv.coe_mk {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
                              { toEquiv := f, map_add' := hf } = f
                              @[simp]
                              theorem MulEquiv.coe_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
                              { toEquiv := f, map_mul' := hf } = f
                              @[simp]
                              theorem AddEquiv.mk_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (e' : NM) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : M), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
                              { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e
                              @[simp]
                              theorem MulEquiv.mk_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (e' : NM) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : M), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
                              { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e
                              @[simp]
                              theorem AddEquiv.toEquiv_eq_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                              f.toEquiv = f
                              @[simp]
                              theorem MulEquiv.toEquiv_eq_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                              f.toEquiv = f
                              @[simp]
                              theorem AddEquiv.toAddHom_eq_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                              f.toAddHom = f
                              @[simp]
                              theorem MulEquiv.toMulHom_eq_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                              f.toMulHom = f
                              @[simp]
                              theorem AddEquiv.coe_toEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                              f = f
                              @[simp]
                              theorem MulEquiv.coe_toEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                              f = f
                              @[simp]
                              theorem AddEquiv.coe_toAddHom {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} :
                              f.toAddHom = f
                              @[simp]
                              theorem MulEquiv.coe_toMulHom {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} :
                              f.toMulHom = f
                              def AddEquiv.mk' {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (h : ∀ (x y : M), f (x + y) = f x + f y) :
                              M ≃+ N

                              Makes an additive isomorphism from a bijection which preserves addition.

                              Equations
                              Instances For
                                def MulEquiv.mk' {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M N) (h : ∀ (x y : M), f (x * y) = f x * f y) :
                                M ≃* N

                                Makes a multiplicative isomorphism from a bijection which preserves multiplication.

                                Equations
                                Instances For
                                  @[deprecated map_add]
                                  theorem AddEquiv.map_add {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) (x : M) (y : M) :
                                  f (x + y) = f x + f y

                                  An additive isomorphism preserves addition.

                                  @[deprecated map_mul]
                                  theorem MulEquiv.map_mul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) (x : M) (y : M) :
                                  f (x * y) = f x * f y

                                  A multiplicative isomorphism preserves multiplication.

                                  theorem AddEquiv.bijective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                  theorem MulEquiv.bijective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                  theorem AddEquiv.injective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                  theorem MulEquiv.injective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                  theorem AddEquiv.surjective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                  theorem MulEquiv.surjective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                  theorem AddEquiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : M} :
                                  e x = e y x = y
                                  theorem MulEquiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : M} :
                                  e x = e y x = y
                                  def AddEquiv.refl (M : Type u_12) [Add M] :
                                  M ≃+ M

                                  The identity map is an additive isomorphism.

                                  Equations
                                  Instances For
                                    theorem AddEquiv.refl.proof_1 (M : Type u_1) [Add M] :
                                    ∀ (x x_1 : M), (Equiv.refl M).toFun (x + x_1) = (Equiv.refl M).toFun (x + x_1)
                                    def MulEquiv.refl (M : Type u_12) [Mul M] :
                                    M ≃* M

                                    The identity map is a multiplicative isomorphism.

                                    Equations
                                    Instances For
                                      instance AddEquiv.instInhabited {M : Type u_6} [Add M] :
                                      Equations
                                      instance MulEquiv.instInhabited {M : Type u_6} [Mul M] :
                                      Equations
                                      @[simp]
                                      theorem AddEquiv.coe_refl {M : Type u_6} [Add M] :
                                      (AddEquiv.refl M) = id
                                      @[simp]
                                      theorem MulEquiv.coe_refl {M : Type u_6} [Mul M] :
                                      (MulEquiv.refl M) = id
                                      @[simp]
                                      theorem AddEquiv.refl_apply {M : Type u_6} [Add M] (m : M) :
                                      @[simp]
                                      theorem MulEquiv.refl_apply {M : Type u_6} [Mul M] (m : M) :
                                      theorem AddEquiv.symm_map_add {M : Type u_12} {N : Type u_13} [Add M] [Add N] (h : M ≃+ N) (x : N) (y : N) :
                                      h.symm (x + y) = h.symm x + h.symm y
                                      theorem MulEquiv.symm_map_mul {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (h : M ≃* N) (x : N) (y : N) :
                                      h.symm (x * y) = h.symm x * h.symm y

                                      An alias for h.symm.map_mul. Introduced to fix the issue in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth

                                      def AddEquiv.symm {M : Type u_12} {N : Type u_13} [Add M] [Add N] (h : M ≃+ N) :
                                      N ≃+ M

                                      The inverse of an isomorphism is an isomorphism.

                                      Equations
                                      • h.symm = { toEquiv := h.symm, map_add' := }
                                      Instances For
                                        def MulEquiv.symm {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (h : M ≃* N) :
                                        N ≃* M

                                        The inverse of an isomorphism is an isomorphism.

                                        Equations
                                        • h.symm = { toEquiv := h.symm, map_mul' := }
                                        Instances For
                                          theorem AddEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} :
                                          f.invFun = f.symm
                                          theorem MulEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} :
                                          f.invFun = f.symm
                                          @[simp]
                                          theorem AddEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                                          (↑f).symm = f.symm
                                          @[simp]
                                          theorem MulEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                                          (↑f).symm = f.symm
                                          @[simp]
                                          theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                                          EquivLike.inv f = f.symm
                                          @[simp]
                                          theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                                          EquivLike.inv f = f.symm
                                          @[simp]
                                          theorem AddEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                                          f.symm = (↑f).symm
                                          @[simp]
                                          theorem MulEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                                          f.symm = (↑f).symm
                                          @[simp]
                                          theorem AddEquiv.symm_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
                                          f.symm.symm = f
                                          @[simp]
                                          theorem MulEquiv.symm_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
                                          f.symm.symm = f
                                          theorem AddEquiv.symm_bijective {M : Type u_6} {N : Type u_7} [Add M] [Add N] :
                                          Function.Bijective AddEquiv.symm
                                          theorem MulEquiv.symm_bijective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
                                          Function.Bijective MulEquiv.symm
                                          @[simp]
                                          theorem AddEquiv.mk_coe' {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (f : NM) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) :
                                          { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm
                                          @[simp]
                                          theorem MulEquiv.mk_coe' {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (f : NM) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) :
                                          { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm
                                          @[simp]
                                          theorem AddEquiv.symm_mk {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y) :
                                          { toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := }
                                          @[simp]
                                          theorem MulEquiv.symm_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M N) (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) :
                                          { toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := }
                                          @[simp]
                                          theorem AddEquiv.refl_symm {M : Type u_6} [Add M] :
                                          @[simp]
                                          theorem MulEquiv.refl_symm {M : Type u_6} [Mul M] :
                                          @[simp]
                                          theorem AddEquiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (y : N) :
                                          e (e.symm y) = y

                                          e.symm is a right inverse of e, written as e (e.symm y) = y.

                                          @[simp]
                                          theorem MulEquiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (y : N) :
                                          e (e.symm y) = y

                                          e.symm is a right inverse of e, written as e (e.symm y) = y.

                                          @[simp]
                                          theorem AddEquiv.symm_apply_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (x : M) :
                                          e.symm (e x) = x

                                          e.symm is a left inverse of e, written as e.symm (e y) = y.

                                          @[simp]
                                          theorem MulEquiv.symm_apply_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (x : M) :
                                          e.symm (e x) = x

                                          e.symm is a left inverse of e, written as e.symm (e y) = y.

                                          @[simp]
                                          theorem AddEquiv.symm_comp_self {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                          e.symm e = id
                                          @[simp]
                                          theorem MulEquiv.symm_comp_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                          e.symm e = id
                                          @[simp]
                                          theorem AddEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                          e e.symm = id
                                          @[simp]
                                          theorem MulEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                          e e.symm = id
                                          theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} :
                                          e x = y x = e.symm y
                                          theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} :
                                          e x = y x = e.symm y
                                          theorem AddEquiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
                                          e.symm x = y x = e y
                                          theorem MulEquiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
                                          e.symm x = y x = e y
                                          theorem AddEquiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
                                          y = e.symm x e y = x
                                          theorem MulEquiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
                                          y = e.symm x e y = x
                                          theorem AddEquiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : Nα) (g : Mα) :
                                          f = g e.symm f e = g
                                          theorem MulEquiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : Nα) (g : Mα) :
                                          f = g e.symm f e = g
                                          theorem AddEquiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : Nα) (g : Mα) :
                                          g e.symm = f g = f e
                                          theorem MulEquiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : Nα) (g : Mα) :
                                          g e.symm = f g = f e
                                          theorem AddEquiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : αM) (g : αN) :
                                          f = e.symm g e f = g
                                          theorem MulEquiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : αM) (g : αN) :
                                          f = e.symm g e f = g
                                          theorem AddEquiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : αM) (g : αN) :
                                          e.symm g = f g = e f
                                          theorem MulEquiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : αM) (g : αN) :
                                          e.symm g = f g = e f
                                          @[simp]
                                          theorem AddEquivClass.apply_coe_symm_apply {α : Type u_12} {β : Type u_13} [Add α] [Add β] {F : Type u_14} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : β) :
                                          e ((↑e).symm x) = x
                                          @[simp]
                                          theorem MulEquivClass.apply_coe_symm_apply {α : Type u_12} {β : Type u_13} [Mul α] [Mul β] {F : Type u_14} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) :
                                          e ((↑e).symm x) = x
                                          @[simp]
                                          theorem AddEquivClass.coe_symm_apply_apply {α : Type u_12} {β : Type u_13} [Add α] [Add β] {F : Type u_14} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : α) :
                                          (↑e).symm (e x) = x
                                          @[simp]
                                          theorem MulEquivClass.coe_symm_apply_apply {α : Type u_12} {β : Type u_13} [Mul α] [Mul β] {F : Type u_14} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) :
                                          (↑e).symm (e x) = x
                                          def AddEquiv.Simps.symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                          NM

                                          See Note [custom simps projection]

                                          Equations
                                          Instances For
                                            def MulEquiv.Simps.symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                            NM

                                            See Note [custom simps projection]

                                            Equations
                                            Instances For
                                              theorem AddEquiv.trans.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) (x : M) (y : M) :
                                              h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y)
                                              def AddEquiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
                                              M ≃+ P

                                              Transitivity of addition-preserving isomorphisms

                                              Equations
                                              • h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_add' := }
                                              Instances For
                                                def MulEquiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
                                                M ≃* P

                                                Transitivity of multiplication-preserving isomorphisms

                                                Equations
                                                • h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_mul' := }
                                                Instances For
                                                  @[simp]
                                                  theorem AddEquiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
                                                  (e₁.trans e₂) = e₂ e₁
                                                  @[simp]
                                                  theorem MulEquiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
                                                  (e₁.trans e₂) = e₂ e₁
                                                  @[simp]
                                                  theorem AddEquiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
                                                  (e₁.trans e₂) m = e₂ (e₁ m)
                                                  @[simp]
                                                  theorem MulEquiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
                                                  (e₁.trans e₂) m = e₂ (e₁ m)
                                                  @[simp]
                                                  theorem AddEquiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
                                                  (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
                                                  @[simp]
                                                  theorem MulEquiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
                                                  (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
                                                  @[simp]
                                                  theorem AddEquiv.symm_trans_self {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                                  e.symm.trans e = AddEquiv.refl N
                                                  @[simp]
                                                  theorem MulEquiv.symm_trans_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                                  e.symm.trans e = MulEquiv.refl N
                                                  @[simp]
                                                  theorem AddEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
                                                  e.trans e.symm = AddEquiv.refl M
                                                  @[simp]
                                                  theorem MulEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
                                                  e.trans e.symm = MulEquiv.refl M
                                                  def AddEquiv.addEquivOfUnique {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [Add M] [Add N] :
                                                  M ≃+ N

                                                  The AddEquiv between two AddMonoids with a unique element.

                                                  Equations
                                                  Instances For
                                                    theorem AddEquiv.addEquivOfUnique.proof_1 {M : Type u_2} {N : Type u_1} [Unique M] [Unique N] [Add M] [Add N] :
                                                    ∀ (x x_1 : M), (Equiv.equivOfUnique M N).toFun (x + x_1) = (Equiv.equivOfUnique M N).toFun x + (Equiv.equivOfUnique M N).toFun x_1
                                                    def MulEquiv.mulEquivOfUnique {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [Mul M] [Mul N] :
                                                    M ≃* N

                                                    The MulEquiv between two monoids with a unique element.

                                                    Equations
                                                    Instances For
                                                      theorem AddEquiv.instUnique.proof_1 {M : Type u_1} {N : Type u_2} [Unique M] [Unique N] [Add M] [Add N] :
                                                      ∀ (x : M ≃+ N), x = default
                                                      instance AddEquiv.instUnique {M : Type u_12} {N : Type u_13} [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
                                                      • AddEquiv.instUnique = { default := AddEquiv.addEquivOfUnique, uniq := }
                                                      instance MulEquiv.instUnique {M : Type u_12} {N : Type u_13} [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
                                                      • MulEquiv.instUnique = { default := MulEquiv.mulEquivOfUnique, uniq := }

                                                      Monoids #

                                                      theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
                                                      (e₁.trans e₂) = (↑e₂).comp e₁
                                                      theorem MulEquiv.coe_monoidHom_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
                                                      (e₁.trans e₂) = (↑e₂).comp e₁
                                                      @[simp]
                                                      theorem AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
                                                      (↑e).comp e.symm = AddMonoidHom.id N
                                                      @[simp]
                                                      theorem MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
                                                      (↑e).comp e.symm = MonoidHom.id N
                                                      @[simp]
                                                      theorem AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
                                                      (↑e.symm).comp e = AddMonoidHom.id M
                                                      @[simp]
                                                      theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
                                                      (↑e.symm).comp e = MonoidHom.id M
                                                      theorem AddEquiv.comp_left_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
                                                      Function.Injective fun (f : N →+ P) => f.comp e
                                                      theorem MulEquiv.comp_left_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
                                                      Function.Injective fun (f : N →* P) => f.comp e
                                                      theorem AddEquiv.comp_right_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
                                                      Function.Injective fun (f : P →+ M) => (↑e).comp f
                                                      theorem MulEquiv.comp_right_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
                                                      Function.Injective fun (f : P →* M) => (↑e).comp f
                                                      theorem AddEquiv.map_zero {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :
                                                      h 0 = 0

                                                      An additive isomorphism of additive monoids sends 0 to 0 (and is hence an additive monoid isomorphism).

                                                      theorem MulEquiv.map_one {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
                                                      h 1 = 1

                                                      A multiplicative isomorphism of monoids sends 1 to 1 (and is hence a monoid isomorphism).

                                                      theorem AddEquiv.map_eq_zero_iff {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
                                                      h x = 0 x = 0
                                                      theorem MulEquiv.map_eq_one_iff {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
                                                      h x = 1 x = 1
                                                      theorem AddEquiv.map_ne_zero_iff {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
                                                      h x 0 x 0
                                                      theorem MulEquiv.map_ne_one_iff {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
                                                      h x 1 x 1
                                                      noncomputable def AddEquiv.ofBijective {M : Type u_12} {N : Type u_13} {F : Type u_14} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective f) :
                                                      M ≃+ N

                                                      A bijective AddSemigroup homomorphism is an isomorphism

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem MulEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
                                                        (MulEquiv.ofBijective f hf) a = f a
                                                        @[simp]
                                                        theorem AddEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
                                                        (AddEquiv.ofBijective f hf) a = f a
                                                        noncomputable def MulEquiv.ofBijective {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective f) :
                                                        M ≃* N

                                                        A bijective Semigroup homomorphism is an isomorphism

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective f) :
                                                          f ((AddEquiv.ofBijective f hf).symm n) = n
                                                          @[simp]
                                                          theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective f) :
                                                          f ((MulEquiv.ofBijective f hf).symm n) = n
                                                          theorem AddEquiv.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) (x : M) (y : M) :
                                                          h.toFun (x + y) = h.toFun x + h.toFun y
                                                          def AddEquiv.toAddMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :
                                                          M →+ N

                                                          Extract the forward direction of an additive equivalence as an addition-preserving function.

                                                          Equations
                                                          • h.toAddMonoidHom = { toFun := h.toFun, map_zero' := , map_add' := }
                                                          Instances For
                                                            def MulEquiv.toMonoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
                                                            M →* N

                                                            Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

                                                            Equations
                                                            • h.toMonoidHom = { toFun := h.toFun, map_one' := , map_mul' := }
                                                            Instances For
                                                              @[simp]
                                                              theorem AddEquiv.coe_toAddMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
                                                              e.toAddMonoidHom = e
                                                              @[simp]
                                                              theorem MulEquiv.coe_toMonoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
                                                              e.toMonoidHom = e
                                                              @[simp]
                                                              theorem AddEquiv.toAddMonoidHom_eq_coe {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) :
                                                              f.toAddMonoidHom = f
                                                              @[simp]
                                                              theorem MulEquiv.toMonoidHom_eq_coe {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M ≃* N) :
                                                              f.toMonoidHom = f
                                                              theorem AddEquiv.toAddMonoidHom_injective {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] :
                                                              Function.Injective AddEquiv.toAddMonoidHom
                                                              theorem MulEquiv.toMonoidHom_injective {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] :
                                                              Function.Injective MulEquiv.toMonoidHom
                                                              theorem AddEquiv.arrowCongr.proof_2 {M : Type u_4} {N : Type u_1} {P : Type u_3} {Q : Type u_2} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (k : NQ) :
                                                              (fun (h : MP) (n : N) => g (h (f.symm n))) ((fun (k : NQ) (m : M) => g.symm (k (f m))) k) = k
                                                              def AddEquiv.arrowCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [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
                                                                theorem AddEquiv.arrowCongr.proof_1 {M : Type u_1} {N : Type u_4} {P : Type u_2} {Q : Type u_3} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) :
                                                                (fun (k : NQ) (m : M) => g.symm (k (f m))) ((fun (h : MP) (n : N) => g (h (f.symm n))) h) = h
                                                                theorem AddEquiv.arrowCongr.proof_3 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (k : MP) :
                                                                { 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 := }.toFun (h + k) = { 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 := }.toFun h + { 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 := }.toFun k
                                                                @[simp]
                                                                theorem MulEquiv.arrowCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) (h : MP) (n : N) :
                                                                (MulEquiv.arrowCongr f g) h n = g (h (f.symm n))
                                                                @[simp]
                                                                theorem AddEquiv.arrowCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (n : N) :
                                                                (AddEquiv.arrowCongr f g) h n = g (h (f.symm n))
                                                                def MulEquiv.arrowCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [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
                                                                  theorem AddEquiv.addMonoidHomCongr.proof_1 {M : Type u_1} {N : Type u_3} {P : Type u_2} {Q : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
                                                                  (fun (k : N →+ Q) => g.symm.toAddMonoidHom.comp (k.comp f.toAddMonoidHom)) ((fun (h : M →+ P) => g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)) h) = h
                                                                  def AddEquiv.addMonoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [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
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    theorem AddEquiv.addMonoidHomCongr.proof_2 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (k : N →+ Q) :
                                                                    (fun (h : M →+ P) => g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)) ((fun (k : N →+ Q) => g.symm.toAddMonoidHom.comp (k.comp f.toAddMonoidHom)) k) = k
                                                                    theorem AddEquiv.addMonoidHomCongr.proof_3 {M : Type u_1} {N : Type u_3} {P : Type u_2} {Q : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) (k : M →+ P) :
                                                                    { toFun := fun (h : M →+ P) => g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom), invFun := fun (k : N →+ Q) => g.symm.toAddMonoidHom.comp (k.comp f.toAddMonoidHom), left_inv := , right_inv := }.toFun (h + k) = { toFun := fun (h : M →+ P) => g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom), invFun := fun (k : N →+ Q) => g.symm.toAddMonoidHom.comp (k.comp f.toAddMonoidHom), left_inv := , right_inv := }.toFun h + { toFun := fun (h : M →+ P) => g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom), invFun := fun (k : N →+ Q) => g.symm.toAddMonoidHom.comp (k.comp f.toAddMonoidHom), left_inv := , right_inv := }.toFun k
                                                                    @[simp]
                                                                    theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
                                                                    (f.addMonoidHomCongr g) h = g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)
                                                                    @[simp]
                                                                    theorem MulEquiv.monoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
                                                                    (f.monoidHomCongr g) h = g.toMonoidHom.comp (h.comp f.symm.toMonoidHom)
                                                                    def MulEquiv.monoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [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
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      theorem AddEquiv.piCongrRight.proof_1 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
                                                                      Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
                                                                      theorem AddEquiv.piCongrRight.proof_3 {η : Type u_1} {Ms : ηType u_3} {Ns : ηType u_2} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (y : (j : η) → Ms j) :
                                                                      { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (es j).symm (x j), left_inv := , right_inv := }.toFun (x + y) = { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (es j).symm (x j), left_inv := , right_inv := }.toFun x + { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (es j).symm (x j), left_inv := , right_inv := }.toFun y
                                                                      def AddEquiv.piCongrRight {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(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
                                                                        theorem AddEquiv.piCongrRight.proof_2 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
                                                                        Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
                                                                        @[simp]
                                                                        theorem AddEquiv.piCongrRight_apply {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
                                                                        (AddEquiv.piCongrRight es) x j = (es j) (x j)
                                                                        @[simp]
                                                                        theorem MulEquiv.piCongrRight_apply {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
                                                                        (MulEquiv.piCongrRight es) x j = (es j) (x j)
                                                                        def MulEquiv.piCongrRight {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(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
                                                                          @[simp]
                                                                          theorem AddEquiv.piCongrRight_refl {η : Type u_12} {Ms : ηType u_13} [(j : η) → Add (Ms j)] :
                                                                          (AddEquiv.piCongrRight fun (j : η) => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
                                                                          @[simp]
                                                                          theorem MulEquiv.piCongrRight_refl {η : Type u_12} {Ms : ηType u_13} [(j : η) → Mul (Ms j)] :
                                                                          (MulEquiv.piCongrRight fun (j : η) => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
                                                                          @[simp]
                                                                          theorem AddEquiv.piCongrRight_symm {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
                                                                          (AddEquiv.piCongrRight es).symm = AddEquiv.piCongrRight fun (i : η) => (es i).symm
                                                                          @[simp]
                                                                          theorem MulEquiv.piCongrRight_symm {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
                                                                          (MulEquiv.piCongrRight es).symm = MulEquiv.piCongrRight fun (i : η) => (es i).symm
                                                                          @[simp]
                                                                          theorem AddEquiv.piCongrRight_trans {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} {Ps : ηType u_15} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
                                                                          (AddEquiv.piCongrRight es).trans (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun (i : η) => (es i).trans (fs i)
                                                                          @[simp]
                                                                          theorem MulEquiv.piCongrRight_trans {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} {Ps : ηType u_15} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
                                                                          (MulEquiv.piCongrRight es).trans (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun (i : η) => (es i).trans (fs i)
                                                                          def AddEquiv.piUnique {ι : Type u_12} (M : ιType u_13) [(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
                                                                            theorem AddEquiv.piUnique.proof_1 {ι : Type u_2} (M : ιType u_1) [(j : ι) → Add (M j)] [Unique ι] :
                                                                            ∀ (x x_1 : (j : ι) → M j), (x + x_1) default = x default + x_1 default
                                                                            @[simp]
                                                                            theorem AddEquiv.piUnique_symm_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) :
                                                                            (AddEquiv.piUnique M).symm x i = uniqueElim x i
                                                                            @[simp]
                                                                            theorem AddEquiv.piUnique_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) :
                                                                            (AddEquiv.piUnique M) f = f default
                                                                            @[simp]
                                                                            theorem MulEquiv.piUnique_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) :
                                                                            (MulEquiv.piUnique M) f = f default
                                                                            @[simp]
                                                                            theorem MulEquiv.piUnique_symm_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) :
                                                                            (MulEquiv.piUnique M).symm x i = uniqueElim x i
                                                                            def MulEquiv.piUnique {ι : Type u_12} (M : ιType u_13) [(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

                                                                              Groups #

                                                                              theorem AddEquiv.map_neg {G : Type u_10} {H : Type u_11} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x : G) :
                                                                              h (-x) = -h x

                                                                              An additive equivalence of additive groups preserves negation.

                                                                              theorem MulEquiv.map_inv {G : Type u_10} {H : Type u_11} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :
                                                                              h x⁻¹ = (h x)⁻¹

                                                                              A multiplicative equivalence of groups preserves inversion.

                                                                              theorem AddEquiv.map_sub {G : Type u_10} {H : Type u_11} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x : G) (y : G) :
                                                                              h (x - y) = h x - h y

                                                                              An additive equivalence of additive groups preserves subtractions.

                                                                              theorem MulEquiv.map_div {G : Type u_10} {H : Type u_11} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) (y : G) :
                                                                              h (x / y) = h x / h y

                                                                              A multiplicative equivalence of groups preserves division.

                                                                              theorem AddHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₂ : f.comp g = AddHom.id N) (x : N) :
                                                                              (f.comp g) x = (AddHom.id N) x
                                                                              theorem AddHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : g.comp f = AddHom.id M) (x : M) :
                                                                              (g.comp f) x = (AddHom.id M) x
                                                                              def AddHom.toAddEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N) :
                                                                              M ≃+ N

                                                                              Given a pair of additive homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive homomorphisms.

                                                                              Equations
                                                                              • f.toAddEquiv g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_add' := }
                                                                              Instances For
                                                                                def MulHom.toMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N) :
                                                                                M ≃* N

                                                                                Given a pair of multiplicative homomorphisms f, g such that g.comp f = id and f.comp g = id, returns a multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for multiplicative homomorphisms.

                                                                                Equations
                                                                                • f.toMulEquiv g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_mul' := }
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem AddHom.toAddEquiv_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N) :
                                                                                  (f.toAddEquiv g h₁ h₂) = f
                                                                                  @[simp]
                                                                                  theorem MulHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N) :
                                                                                  (f.toMulEquiv g h₁ h₂) = f
                                                                                  @[simp]
                                                                                  theorem AddHom.toAddEquiv_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N) :
                                                                                  (f.toAddEquiv g h₁ h₂).symm = g
                                                                                  @[simp]
                                                                                  theorem MulHom.toMulEquiv_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N) :
                                                                                  (f.toMulEquiv g h₁ h₂).symm = g
                                                                                  def AddMonoidHom.toAddEquiv {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N) :
                                                                                  M ≃+ N

                                                                                  Given a pair of additive monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

                                                                                  Equations
                                                                                  • f.toAddEquiv g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_add' := }
                                                                                  Instances For
                                                                                    theorem AddMonoidHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (x : M) :
                                                                                    (g.comp f) x = (AddMonoidHom.id M) x
                                                                                    theorem AddMonoidHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₂ : f.comp g = AddMonoidHom.id N) (x : N) :
                                                                                    (f.comp g) x = (AddMonoidHom.id N) x
                                                                                    @[simp]
                                                                                    theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N) :
                                                                                    (f.toAddEquiv g h₁ h₂).symm = g
                                                                                    @[simp]
                                                                                    theorem AddMonoidHom.toAddEquiv_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N) :
                                                                                    (f.toAddEquiv g h₁ h₂) = f
                                                                                    @[simp]
                                                                                    theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N) :
                                                                                    (f.toMulEquiv g h₁ h₂).symm = g
                                                                                    @[simp]
                                                                                    theorem MonoidHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N) :
                                                                                    (f.toMulEquiv g h₁ h₂) = f
                                                                                    def MonoidHom.toMulEquiv {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N) :
                                                                                    M ≃* N

                                                                                    Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns a multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.

                                                                                    Equations
                                                                                    • f.toMulEquiv g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_mul' := }
                                                                                    Instances For
                                                                                      def Equiv.neg (G : Type u_10) [InvolutiveNeg G] :

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

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Equiv.inv_apply (G : Type u_10) [InvolutiveInv G] :
                                                                                        (Equiv.inv G) = Inv.inv
                                                                                        @[simp]
                                                                                        theorem Equiv.neg_apply (G : Type u_10) [InvolutiveNeg G] :
                                                                                        (Equiv.neg G) = Neg.neg
                                                                                        def Equiv.inv (G : Type u_10) [InvolutiveInv G] :

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

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          @[simp]