Documentation

Mathlib.Algebra.Group.Equiv.Defs

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.

Main definitions #

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

@[simp]
theorem EmbeddingLike.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
@[simp]
theorem EmbeddingLike.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
theorem EmbeddingLike.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
theorem EmbeddingLike.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
structure AddEquiv (A : Type u_9) (B : Type u_10) [Add A] [Add B] extends A B, A →ₙ+ B :
Type (max u_10 u_9)

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

Instances For
    class AddEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [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
      structure MulEquiv (M : Type u_9) (N : Type u_10) [Mul M] [Mul N] extends M N, M →ₙ* N :
      Type (max u_10 u_9)

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

      Instances For
        theorem MulEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] :
        theorem AddEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Add α] [Add β] :
        class MulEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [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
          @[deprecated EmbeddingLike.map_eq_one_iff (since := "2024-11-10")]
          theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :

          Alias of EmbeddingLike.map_eq_one_iff.

          @[deprecated EmbeddingLike.map_eq_zero_iff (since := "2024-11-10")]
          theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
          @[deprecated EmbeddingLike.map_ne_one_iff (since := "2024-11-10")]
          theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :

          Alias of EmbeddingLike.map_ne_one_iff.

          @[deprecated EmbeddingLike.map_ne_zero_iff (since := "2024-11-10")]
          theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
          @[instance 100]
          instance MulEquivClass.instMulHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] :
          @[instance 100]
          instance AddEquivClass.instAddHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] :
          @[instance 100]
          instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
          @[instance 100]
          instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [AddZeroClass M] [AddZeroClass N] [AddEquivClass F M N] :
          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
            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
              instance instCoeTCMulEquivOfMulEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :

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

              Equations
              instance instCoeTCAddEquivOfAddEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :

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

              Equations
              instance MulEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
              Equations
              instance AddEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
              Equations
              instance MulEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
              CoeFun (M ≃* N) fun (x : M ≃* N) => MN
              Equations
              instance AddEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
              CoeFun (M ≃+ N) fun (x : M ≃+ N) => MN
              Equations
              instance MulEquiv.instMulEquivClass {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
              instance AddEquiv.instAddEquivClass {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
              theorem AddEquiv.ext {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f 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 MulEquiv.ext {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f 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 MulEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} {x x' : M} :
              x = x'f x = f x'
              theorem AddEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} {x x' : M} :
              x = x'f x = f x'
              theorem MulEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : f = g) (x : M) :
              f x = g x
              theorem AddEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : f = g) (x : M) :
              f x = g x
              @[simp]
              theorem MulEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
              @[simp]
              theorem AddEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
              @[simp]
              theorem MulEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
              @[simp]
              theorem AddEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
              @[simp]
              theorem MulEquiv.toMulHom_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :

              The simp-normal form to turn something into a MulHom is via MulHomClass.toMulHom.

              @[simp]
              theorem AddEquiv.toAddHom_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
              theorem MulEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
              f.toFun = f
              theorem AddEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
              f.toFun = f
              @[simp]
              theorem MulEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :

              simp-normal form of toFun_eq_coe.

              @[simp]
              theorem AddEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
              @[simp]
              theorem MulEquiv.coe_toMulHom {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
              @[simp]
              theorem AddEquiv.coe_toAddHom {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
              def MulEquiv.mk' {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M N) (h : ∀ (x y : M), f (x * y) = f x * f y) :

              Makes a multiplicative isomorphism from a bijection which preserves multiplication.

              Equations
              Instances For
                def AddEquiv.mk' {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M N) (h : ∀ (x y : M), f (x + y) = f x + f y) :

                Makes an additive isomorphism from a bijection which preserves addition.

                Equations
                Instances For
                  @[deprecated map_mul (since := "2024-08-08")]
                  theorem MulEquiv.map_mul {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) (x y : M) :
                  f (x * y) = f x * f y

                  A multiplicative isomorphism preserves multiplication.

                  @[deprecated map_add (since := "2024-08-08")]
                  theorem AddEquiv.map_add {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (x y : M) :
                  f (x + y) = f x + f y

                  An additive isomorphism preserves addition.

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

                  The identity map is a multiplicative isomorphism.

                  Equations
                  Instances For
                    def AddEquiv.refl (M : Type u_9) [Add M] :

                    The identity map is an additive isomorphism.

                    Equations
                    Instances For
                      instance MulEquiv.instInhabited {M : Type u_4} [Mul M] :
                      Equations
                      instance AddEquiv.instInhabited {M : Type u_4} [Add M] :
                      Equations
                      @[simp]
                      theorem MulEquiv.coe_refl {M : Type u_4} [Mul M] :
                      @[simp]
                      theorem AddEquiv.coe_refl {M : Type u_4} [Add M] :
                      @[simp]
                      theorem MulEquiv.refl_apply {M : Type u_4} [Mul M] (m : M) :
                      (refl M) m = m
                      @[simp]
                      theorem AddEquiv.refl_apply {M : Type u_4} [Add M] (m : M) :
                      (refl M) m = m
                      theorem MulEquiv.symm_map_mul {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) (x y : N) :

                      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

                      theorem AddEquiv.symm_map_add {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) (x y : N) :
                      def MulEquiv.symm {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) :

                      The inverse of an isomorphism is an isomorphism.

                      Equations
                      Instances For
                        def AddEquiv.symm {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) :

                        The inverse of an isomorphism is an isomorphism.

                        Equations
                        Instances For
                          theorem MulEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
                          theorem AddEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
                          @[simp]
                          theorem MulEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :

                          simp-normal form of invFun_eq_symm.

                          @[simp]
                          theorem AddEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
                          @[simp]
                          theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
                          @[simp]
                          theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
                          @[simp]
                          theorem MulEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
                          @[simp]
                          theorem AddEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
                          @[simp]
                          theorem MulEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
                          @[simp]
                          theorem AddEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
                          @[simp]
                          theorem MulEquiv.symm_mk {M : Type u_4} {N : Type u_5} [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.symm_mk {M : Type u_4} {N : Type u_5} [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.refl_symm {M : Type u_4} [Mul M] :
                          @[simp]
                          theorem AddEquiv.refl_symm {M : Type u_4} [Add M] :
                          @[simp]
                          theorem MulEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (y : N) :

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

                          @[simp]
                          theorem AddEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (y : N) :

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

                          @[simp]
                          theorem MulEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [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_apply_apply {M : Type u_4} {N : Type u_5} [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_comp_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
                          @[simp]
                          theorem AddEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
                          @[simp]
                          theorem MulEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
                          @[simp]
                          theorem AddEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
                          theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} :
                          theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} :
                          theorem MulEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
                          e.symm x = y x = e y
                          theorem AddEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
                          e.symm x = y x = e y
                          theorem MulEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
                          theorem AddEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
                          theorem MulEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : Nα) (g : Mα) :
                          f = g e.symm f e = g
                          theorem AddEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : Nα) (g : Mα) :
                          f = g e.symm f e = g
                          theorem MulEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : Nα) (g : Mα) :
                          g e.symm = f g = f e
                          theorem AddEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : Nα) (g : Mα) :
                          g e.symm = f g = f e
                          theorem MulEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : αM) (g : αN) :
                          theorem AddEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : αM) (g : αN) :
                          theorem MulEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : αM) (g : αN) :
                          theorem AddEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : αM) (g : αN) :
                          @[simp]
                          theorem MulEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) :
                          @[simp]
                          theorem AddEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : β) :
                          @[simp]
                          theorem MulEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) :
                          (↑e).symm (e x) = x
                          @[simp]
                          theorem AddEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : α) :
                          (↑e).symm (e x) = x
                          def MulEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
                          NM

                          See Note [custom simps projection]

                          Equations
                          Instances For
                            def AddEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
                            NM

                            See Note [custom simps projection]

                            Equations
                            Instances For
                              def MulEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :

                              Transitivity of multiplication-preserving isomorphisms

                              Equations
                              Instances For
                                def AddEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :

                                Transitivity of addition-preserving isomorphisms

                                Equations
                                Instances For
                                  @[simp]
                                  theorem MulEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
                                  @[simp]
                                  theorem AddEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
                                  @[simp]
                                  theorem MulEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
                                  (e₁.trans e₂) m = e₂ (e₁ m)
                                  @[simp]
                                  theorem AddEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
                                  (e₁.trans e₂) m = e₂ (e₁ m)
                                  @[simp]
                                  theorem MulEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [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_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [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_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
                                  @[simp]
                                  theorem AddEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
                                  @[simp]
                                  theorem MulEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
                                  @[simp]
                                  theorem AddEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :

                                  Monoids #

                                  theorem MulEquiv.coe_monoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
                                  (e₁.trans e₂) = (↑e₂).comp e₁
                                  theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
                                  (e₁.trans e₂) = (↑e₂).comp e₁
                                  theorem MulEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
                                  Function.Injective fun (f : N →* P) => f.comp e
                                  theorem AddEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
                                  Function.Injective fun (f : N →+ P) => f.comp e
                                  theorem MulEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
                                  Function.Injective fun (f : P →* M) => (↑e).comp f
                                  theorem AddEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
                                  Function.Injective fun (f : P →+ M) => (↑e).comp f
                                  theorem MulEquiv.map_one {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :

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

                                  theorem AddEquiv.map_zero {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :

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

                                  theorem MulEquiv.map_eq_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
                                  theorem AddEquiv.map_eq_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
                                  theorem MulEquiv.map_ne_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
                                  theorem AddEquiv.map_ne_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
                                  noncomputable def MulEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective f) :

                                  A bijective Semigroup homomorphism is an isomorphism

                                  Equations
                                  Instances For
                                    noncomputable def AddEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective f) :

                                    A bijective AddSemigroup homomorphism is an isomorphism

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem AddEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
                                      (ofBijective f hf) a = f a
                                      @[simp]
                                      theorem MulEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
                                      (ofBijective f hf) a = f a
                                      @[simp]
                                      theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective f) :
                                      @[simp]
                                      theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective f) :
                                      def MulEquiv.toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :

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

                                      Equations
                                      Instances For
                                        def AddEquiv.toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :

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

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem MulEquiv.coe_toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
                                          @[simp]
                                          theorem AddEquiv.coe_toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
                                          @[simp]
                                          theorem MulEquiv.toMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M ≃* N) :
                                          @[simp]
                                          theorem AddEquiv.toAddMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) :

                                          Groups #

                                          theorem MulEquiv.map_inv {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :

                                          A multiplicative equivalence of groups preserves inversion.

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

                                          An additive equivalence of additive groups preserves negation.

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

                                          A multiplicative equivalence of groups preserves division.

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

                                          An additive equivalence of additive groups preserves subtractions.

                                          def MulHom.toMulEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id 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
                                            def AddHom.toAddEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id 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
                                              @[simp]
                                              theorem AddHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                              (f.toAddEquiv g h₁ h₂) = f
                                              @[simp]
                                              theorem MulHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                              (f.toMulEquiv g h₁ h₂) = f
                                              @[simp]
                                              theorem AddHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                              (f.toAddEquiv g h₁ h₂).symm = g
                                              @[simp]
                                              theorem MulHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                              (f.toMulEquiv g h₁ h₂).symm = g
                                              def MonoidHom.toMulEquiv {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id 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 AddMonoidHom.toAddEquiv {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id 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
                                                  @[simp]
                                                  theorem MonoidHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                                  (f.toMulEquiv g h₁ h₂) = f
                                                  @[simp]
                                                  theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                                  (f.toMulEquiv g h₁ h₂).symm = g
                                                  @[simp]
                                                  theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                                  (f.toAddEquiv g h₁ h₂).symm = g
                                                  @[simp]
                                                  theorem AddMonoidHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
                                                  (f.toAddEquiv g h₁ h₂) = f