Documentation

Mathlib.Algebra.Group.Subsemigroup.Operations

Operations on Subsemigroups #

In this file we define various operations on Subsemigroups and MulHoms.

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on MulHoms #

Implementation notes #

This file follows closely GroupTheory/Submonoid/Operations.lean, omitting only that which is necessary.

Tags #

subsemigroup, range, product, map, comap

Conversion to/from Additive/Multiplicative #

@[simp]
theorem Subsemigroup.toAddSubsemigroup_symm_apply_coe {M : Type u_1} [Mul M] (S : AddSubsemigroup (Additive M)) :
((RelIso.symm Subsemigroup.toAddSubsemigroup) S) = Additive.ofMul ⁻¹' S
@[simp]
theorem Subsemigroup.toAddSubsemigroup_apply_coe {M : Type u_1} [Mul M] (S : Subsemigroup M) :
(Subsemigroup.toAddSubsemigroup S) = Additive.toMul ⁻¹' S

Subsemigroups of semigroup M are isomorphic to additive subsemigroups of Additive M.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline]

    Additive subsemigroups of an additive semigroup Additive M are isomorphic to subsemigroups of M.

    Equations
    • AddSubsemigroup.toSubsemigroup' = Subsemigroup.toAddSubsemigroup.symm
    Instances For
      theorem Subsemigroup.toAddSubsemigroup_closure {M : Type u_1} [Mul M] (S : Set M) :
      Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (Additive.toMul ⁻¹' S)
      theorem AddSubsemigroup.toSubsemigroup'_closure {M : Type u_1} [Mul M] (S : Set (Additive M)) :
      AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (Additive.ofMul ⁻¹' S)
      @[simp]
      theorem AddSubsemigroup.toSubsemigroup_symm_apply_coe {A : Type u_5} [Add A] (S : Subsemigroup (Multiplicative A)) :
      ((RelIso.symm AddSubsemigroup.toSubsemigroup) S) = Multiplicative.ofAdd ⁻¹' S
      @[simp]
      theorem AddSubsemigroup.toSubsemigroup_apply_coe {A : Type u_5} [Add A] (S : AddSubsemigroup A) :
      (AddSubsemigroup.toSubsemigroup S) = Multiplicative.toAdd ⁻¹' S

      Additive subsemigroups of an additive semigroup A are isomorphic to multiplicative subsemigroups of Multiplicative A.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]

        Subsemigroups of a semigroup Multiplicative A are isomorphic to additive subsemigroups of A.

        Equations
        • Subsemigroup.toAddSubsemigroup' = AddSubsemigroup.toSubsemigroup.symm
        Instances For
          theorem AddSubsemigroup.toSubsemigroup_closure {A : Type u_5} [Add A] (S : Set A) :
          AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (Multiplicative.toAdd ⁻¹' S)
          theorem Subsemigroup.toAddSubsemigroup'_closure {A : Type u_5} [Add A] (S : Set (Multiplicative A)) :
          Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (Multiplicative.ofAdd ⁻¹' S)

          comap and map #

          def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup N) :

          The preimage of an AddSubsemigroup along an AddSemigroup homomorphism is an AddSubsemigroup.

          Equations
          Instances For
            theorem AddSubsemigroup.comap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup N) :
            ∀ {a b : M}, a f ⁻¹' Sb f ⁻¹' Sf (a + b) S
            def Subsemigroup.comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup N) :

            The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.

            Equations
            Instances For
              @[simp]
              theorem AddSubsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup N) (f : AddHom M N) :
              (AddSubsemigroup.comap f S) = f ⁻¹' S
              @[simp]
              theorem Subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup N) (f : M →ₙ* N) :
              (Subsemigroup.comap f S) = f ⁻¹' S
              @[simp]
              theorem AddSubsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M} :
              @[simp]
              theorem Subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : Subsemigroup N} {f : M →ₙ* N} {x : M} :
              theorem AddSubsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : AddSubsemigroup P) (g : AddHom N P) (f : AddHom M N) :
              theorem Subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : Subsemigroup P) (g : N →ₙ* P) (f : M →ₙ* N) :
              @[simp]
              def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :

              The image of an AddSubsemigroup along an AddSemigroup homomorphism is an AddSubsemigroup.

              Equations
              Instances For
                theorem AddSubsemigroup.map.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
                ∀ {a b : N}, a f '' Sb f '' Sa + b f '' S
                def Subsemigroup.map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :

                The image of a subsemigroup along a semigroup homomorphism is a subsemigroup.

                Equations
                Instances For
                  @[simp]
                  theorem AddSubsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
                  (AddSubsemigroup.map f S) = f '' S
                  @[simp]
                  theorem Subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :
                  (Subsemigroup.map f S) = f '' S
                  @[simp]
                  theorem AddSubsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : AddSubsemigroup M} {y : N} :
                  y AddSubsemigroup.map f S xS, f x = y
                  @[simp]
                  theorem Subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {y : N} :
                  y Subsemigroup.map f S xS, f x = y
                  theorem AddSubsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {S : AddSubsemigroup M} {x : M} (hx : x S) :
                  theorem Subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {S : Subsemigroup M} {x : M} (hx : x S) :
                  theorem AddSubsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) (x : S) :
                  theorem Subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) (x : S) :
                  theorem AddSubsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : AddSubsemigroup M) (g : AddHom N P) (f : AddHom M N) :
                  theorem Subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : Subsemigroup M) (g : N →ₙ* P) (f : M →ₙ* N) :
                  @[simp]
                  theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective f) {S : AddSubsemigroup M} {x : M} :
                  @[simp]
                  theorem Subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {x : M} :
                  theorem Subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} :
                  theorem Subsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :
                  theorem Subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :
                  theorem Subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {f : M →ₙ* N} :
                  theorem Subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : Subsemigroup N} {f : M →ₙ* N} :
                  theorem AddSubsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} :
                  theorem Subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :
                  theorem AddSubsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} :
                  theorem Subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :
                  @[simp]
                  theorem Subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (T : Subsemigroup M) (f : M →ₙ* N) :
                  theorem AddSubsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ιAddSubsemigroup M) :
                  AddSubsemigroup.map f (iSup s) = ⨆ (i : ι), AddSubsemigroup.map f (s i)
                  theorem Subsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ιSubsemigroup M) :
                  Subsemigroup.map f (iSup s) = ⨆ (i : ι), Subsemigroup.map f (s i)
                  theorem Subsemigroup.map_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) :
                  theorem AddSubsemigroup.map_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} [Nonempty ι] (f : AddHom M N) (hf : Function.Injective f) (s : ιAddSubsemigroup M) :
                  AddSubsemigroup.map f (iInf s) = ⨅ (i : ι), AddSubsemigroup.map f (s i)
                  theorem Subsemigroup.map_iInf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} [Nonempty ι] (f : M →ₙ* N) (hf : Function.Injective f) (s : ιSubsemigroup M) :
                  Subsemigroup.map f (iInf s) = ⨅ (i : ι), Subsemigroup.map f (s i)
                  theorem Subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup N) (T : Subsemigroup N) (f : M →ₙ* N) :
                  theorem AddSubsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ιAddSubsemigroup N) :
                  theorem Subsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ιSubsemigroup N) :
                  Subsemigroup.comap f (iInf s) = ⨅ (i : ι), Subsemigroup.comap f (s i)
                  @[simp]
                  theorem AddSubsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                  @[simp]
                  theorem Subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                  @[simp]
                  theorem AddSubsemigroup.comap_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                  @[simp]
                  theorem Subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                  @[simp]
                  @[simp]
                  theorem Subsemigroup.map_id {M : Type u_1} [Mul M] (S : Subsemigroup M) :
                  theorem AddSubsemigroup.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective f) (S : AddSubsemigroup M) (x : M) :

                  map f and comap f form a GaloisCoinsertion when f is injective.

                  Equations
                  Instances For

                    map f and comap f form a GaloisCoinsertion when f is injective.

                    Equations
                    Instances For
                      theorem Subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective f) (S : Subsemigroup M) :
                      theorem AddSubsemigroup.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : Function.Injective f) (S : ιAddSubsemigroup M) :
                      AddSubsemigroup.comap f (⨅ (i : ι), AddSubsemigroup.map f (S i)) = iInf S
                      theorem Subsemigroup.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : Function.Injective f) (S : ιSubsemigroup M) :
                      Subsemigroup.comap f (⨅ (i : ι), Subsemigroup.map f (S i)) = iInf S
                      theorem AddSubsemigroup.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : Function.Injective f) (S : ιAddSubsemigroup M) :
                      AddSubsemigroup.comap f (⨆ (i : ι), AddSubsemigroup.map f (S i)) = iSup S
                      theorem Subsemigroup.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : Function.Injective f) (S : ιSubsemigroup M) :
                      Subsemigroup.comap f (⨆ (i : ι), Subsemigroup.map f (S i)) = iSup S
                      theorem Subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {T : Subsemigroup M} :
                      theorem AddSubsemigroup.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective f) (S : AddSubsemigroup N) (x : N) (h : x S) :

                      map f and comap f form a GaloisInsertion when f is surjective.

                      Equations
                      Instances For

                        map f and comap f form a GaloisInsertion when f is surjective.

                        Equations
                        Instances For
                          theorem AddSubsemigroup.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : Function.Surjective f) (S : ιAddSubsemigroup N) :
                          AddSubsemigroup.map f (⨅ (i : ι), AddSubsemigroup.comap f (S i)) = iInf S
                          theorem Subsemigroup.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : Function.Surjective f) (S : ιSubsemigroup N) :
                          Subsemigroup.map f (⨅ (i : ι), Subsemigroup.comap f (S i)) = iInf S
                          theorem AddSubsemigroup.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : Function.Surjective f) (S : ιAddSubsemigroup N) :
                          AddSubsemigroup.map f (⨆ (i : ι), AddSubsemigroup.comap f (S i)) = iSup S
                          theorem Subsemigroup.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : Function.Surjective f) (S : ιSubsemigroup N) :
                          Subsemigroup.map f (⨆ (i : ι), Subsemigroup.comap f (S i)) = iSup S
                          @[instance 900]
                          instance AddMemClass.add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
                          Add S'

                          An additive submagma of an additive magma inherits an addition.

                          Equations
                          theorem AddMemClass.add.proof_1 {M : Type u_1} {A : Type u_2} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (a : S') (b : S') :
                          a + b S'
                          @[instance 900]
                          instance MulMemClass.mul {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
                          Mul S'

                          A submagma of a magma inherits a multiplication.

                          Equations
                          @[simp]
                          theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x : S') (y : S') :
                          (x + y) = x + y
                          @[simp]
                          theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x : S') (y : S') :
                          (x * y) = x * y
                          @[simp]
                          theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
                          x, hx + y, hy = x + y,
                          @[simp]
                          theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
                          x, hx * y, hy = x * y,
                          theorem AddMemClass.add_def {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x : S') (y : S') :
                          x + y = x + y,
                          theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x : S') (y : S') :
                          x * y = x * y,
                          theorem AddMemClass.toAddSemigroup.proof_2 {M : Type u_1} [AddSemigroup M] {A : Type u_2} [SetLike A M] [AddMemClass A M] (S : A) :
                          ∀ (x x_1 : S), (x + x_1) = (x + x_1)
                          instance AddMemClass.toAddSemigroup {M : Type u_6} [AddSemigroup M] {A : Type u_7} [SetLike A M] [AddMemClass A M] (S : A) :

                          An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

                          Equations
                          theorem AddMemClass.toAddSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                          Function.Injective fun (a : S) => a
                          instance MulMemClass.toSemigroup {M : Type u_6} [Semigroup M] {A : Type u_7} [SetLike A M] [MulMemClass A M] (S : A) :

                          A subsemigroup of a semigroup inherits a semigroup structure.

                          Equations
                          theorem AddMemClass.toAddCommSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                          Function.Injective fun (a : S) => a
                          theorem AddMemClass.toAddCommSemigroup.proof_2 {M : Type u_1} [AddCommSemigroup M] {A : Type u_2} [SetLike A M] [AddMemClass A M] (S : A) :
                          ∀ (x x_1 : S), (x + x_1) = (x + x_1)
                          instance MulMemClass.toCommSemigroup {M : Type u_7} [CommSemigroup M] {A : Type u_6} [SetLike A M] [MulMemClass A M] (S : A) :

                          A subsemigroup of a CommSemigroup is a CommSemigroup.

                          Equations
                          theorem AddMemClass.subtype.proof_1 {M : Type u_1} {A : Type u_2} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
                          ∀ (x x_1 : S'), (x + x_1) = (x + x_1)
                          def AddMemClass.subtype {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
                          AddHom (↥S') M

                          The natural semigroup hom from an AddSubsemigroup of AddSubsemigroup M to M.

                          Equations
                          Instances For
                            def MulMemClass.subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
                            S' →ₙ* M

                            The natural semigroup hom from a subsemigroup of semigroup M to M.

                            Equations
                            Instances For
                              @[simp]
                              theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
                              (AddMemClass.subtype S') = Subtype.val
                              @[simp]
                              theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
                              (MulMemClass.subtype S') = Subtype.val
                              def AddSubsemigroup.topEquiv {M : Type u_1} [Add M] :
                              ≃+ M

                              The top additive subsemigroup is isomorphic to the additive semigroup.

                              Equations
                              • AddSubsemigroup.topEquiv = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_add' := }
                              Instances For
                                theorem AddSubsemigroup.topEquiv.proof_2 {M : Type u_1} [Add M] :
                                ∀ (x : M), (fun (x : ) => x) ((fun (x : M) => x, ) x) = (fun (x : ) => x) ((fun (x : M) => x, ) x)
                                theorem AddSubsemigroup.topEquiv.proof_1 {M : Type u_1} [Add M] (x : ) :
                                x, = x
                                theorem AddSubsemigroup.topEquiv.proof_3 {M : Type u_1} [Add M] :
                                ∀ (x x_1 : ), { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1)
                                @[simp]
                                theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [Add M] (x : ) :
                                AddSubsemigroup.topEquiv x = x
                                @[simp]
                                theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Mul M] (x : M) :
                                (Subsemigroup.topEquiv.symm x) = x
                                @[simp]
                                theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Add M] (x : M) :
                                (AddSubsemigroup.topEquiv.symm x) = x
                                @[simp]
                                theorem Subsemigroup.topEquiv_apply {M : Type u_1} [Mul M] (x : ) :
                                Subsemigroup.topEquiv x = x
                                def Subsemigroup.topEquiv {M : Type u_1} [Mul M] :
                                ≃* M

                                The top subsemigroup is isomorphic to the semigroup.

                                Equations
                                • Subsemigroup.topEquiv = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_mul' := }
                                Instances For
                                  @[simp]
                                  theorem AddSubsemigroup.topEquiv_toAddHom {M : Type u_1} [Add M] :
                                  AddSubsemigroup.topEquiv = AddMemClass.subtype
                                  @[simp]
                                  theorem Subsemigroup.topEquiv_toMulHom {M : Type u_1} [Mul M] :
                                  Subsemigroup.topEquiv = MulMemClass.subtype
                                  theorem AddSubsemigroup.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
                                  ∀ (x x_1 : S), (Equiv.Set.image (⇑f) (↑S) hf).toFun (x + x_1) = (Equiv.Set.image (⇑f) (↑S) hf).toFun x + (Equiv.Set.image (⇑f) (↑S) hf).toFun x_1
                                  noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :

                                  An additive subsemigroup is isomorphic to its image under an injective function

                                  Equations
                                  • S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := }
                                  Instances For
                                    noncomputable def Subsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) :
                                    S ≃* (Subsemigroup.map f S)

                                    A subsemigroup is isomorphic to its image under an injective function

                                    Equations
                                    • S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := }
                                    Instances For
                                      @[simp]
                                      theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) (x : S) :
                                      ((S.equivMapOfInjective f hf) x) = f x
                                      @[simp]
                                      theorem Subsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) (x : S) :
                                      ((S.equivMapOfInjective f hf) x) = f x
                                      @[simp]
                                      @[simp]
                                      theorem Subsemigroup.closure_closure_coe_preimage {M : Type u_1} [Mul M] {s : Set M} :
                                      def AddSubsemigroup.prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :

                                      Given AddSubsemigroups s, t of AddSemigroups A, B respectively, s × t as an AddSubsemigroup of A × B.

                                      Equations
                                      • s.prod t = { carrier := s ×ˢ t, add_mem' := }
                                      Instances For
                                        theorem AddSubsemigroup.prod.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                        ∀ {a b : M × N}, a s ×ˢ tb s ×ˢ t(a + b).1 s (a + b).2 t
                                        def Subsemigroup.prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :

                                        Given Subsemigroups s, t of semigroups M, N respectively, s × t as a subsemigroup of M × N.

                                        Equations
                                        • s.prod t = { carrier := s ×ˢ t, mul_mem' := }
                                        Instances For
                                          theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                          (s.prod t) = s ×ˢ t
                                          theorem Subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
                                          (s.prod t) = s ×ˢ t
                                          theorem AddSubsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} {p : M × N} :
                                          p s.prod t p.1 s p.2 t
                                          theorem Subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {p : M × N} :
                                          p s.prod t p.1 s p.2 t
                                          theorem AddSubsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s₁ : AddSubsemigroup M} {s₂ : AddSubsemigroup M} {t₁ : AddSubsemigroup N} {t₂ : AddSubsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
                                          s₁.prod t₁ s₂.prod t₂
                                          theorem Subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s₁ : Subsemigroup M} {s₂ : Subsemigroup M} {t₁ : Subsemigroup N} {t₂ : Subsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
                                          s₁.prod t₁ s₂.prod t₂
                                          theorem AddSubsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) :
                                          theorem Subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) :
                                          theorem AddSubsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup N) :
                                          theorem Subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup N) :
                                          @[simp]
                                          theorem AddSubsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                          .prod =
                                          @[simp]
                                          theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
                                          .prod =
                                          theorem AddSubsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                          .prod =
                                          theorem Subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
                                          .prod =
                                          theorem AddSubsemigroup.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                          ∀ (x x_1 : (s.prod t)), (Equiv.Set.prod s t).toFun (x + x_1) = (Equiv.Set.prod s t).toFun (x + x_1)
                                          def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                          (s.prod t) ≃+ s × t

                                          The product of additive subsemigroups is isomorphic to their product as additive semigroups

                                          Equations
                                          Instances For
                                            theorem AddSubsemigroup.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                            def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
                                            (s.prod t) ≃* s × t

                                            The product of subsemigroups is isomorphic to their product as semigroups.

                                            Equations
                                            Instances For
                                              theorem AddSubsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M ≃+ N} {K : AddSubsemigroup M} {x : N} :
                                              x AddSubsemigroup.map (↑f) K f.symm x K
                                              theorem Subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M ≃* N} {K : Subsemigroup M} {x : N} :
                                              x Subsemigroup.map (↑f) K f.symm x K
                                              theorem AddSubsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) (K : AddSubsemigroup M) :
                                              theorem Subsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) (K : Subsemigroup M) :
                                              Subsemigroup.map (↑f) K = Subsemigroup.comap (↑f.symm) K
                                              theorem AddSubsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : N ≃+ M) (K : AddSubsemigroup M) :
                                              theorem Subsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : N ≃* M) (K : Subsemigroup M) :
                                              Subsemigroup.comap (↑f) K = Subsemigroup.map (↑f.symm) K
                                              @[simp]
                                              theorem AddSubsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) :
                                              @[simp]
                                              theorem Subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) :
                                              theorem AddSubsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} {u : AddSubsemigroup (M × N)} :
                                              theorem Subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (M × N)} :
                                              def AddHom.srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :

                                              The range of an AddHom is an AddSubsemigroup.

                                              Equations
                                              Instances For
                                                theorem AddHom.srange.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) :
                                                Set.range f = f '' Set.univ
                                                def MulHom.srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :

                                                The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern].

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem AddHom.coe_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                                                  f.srange = Set.range f
                                                  @[simp]
                                                  theorem MulHom.coe_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                  f.srange = Set.range f
                                                  @[simp]
                                                  theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {y : N} :
                                                  y f.srange ∃ (x : M), f x = y
                                                  @[simp]
                                                  theorem MulHom.mem_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {y : N} :
                                                  y f.srange ∃ (x : M), f x = y
                                                  @[simp]
                                                  theorem AddHom.srange_mk {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : MN) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
                                                  { toFun := f, map_add' := hf }.srange = { carrier := Set.range f, add_mem' := }
                                                  @[simp]
                                                  theorem MulHom.srange_mk {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : MN) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
                                                  { toFun := f, map_mul' := hf }.srange = { carrier := Set.range f, mul_mem' := }
                                                  theorem AddHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                                                  theorem MulHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                  theorem AddHom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) :
                                                  AddSubsemigroup.map g f.srange = (g.comp f).srange
                                                  theorem MulHom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
                                                  Subsemigroup.map g f.srange = (g.comp f).srange
                                                  theorem AddHom.srange_top_iff_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] {f : AddHom M N} :
                                                  theorem MulHom.srange_top_iff_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] {f : M →ₙ* N} :
                                                  @[simp]
                                                  theorem AddHom.srange_top_of_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (hf : Function.Surjective f) :
                                                  f.srange =

                                                  The range of a surjective AddSemigroup hom is the whole of the codomain.

                                                  @[simp]
                                                  theorem MulHom.srange_top_of_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :
                                                  f.srange =

                                                  The range of a surjective semigroup hom is the whole of the codomain.

                                                  theorem AddHom.map_mclosure {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (s : Set M) :

                                                  The image under an AddSemigroup hom of the AddSubsemigroup generated by a set equals the AddSubsemigroup generated by the image of the set.

                                                  theorem MulHom.map_mclosure {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (s : Set M) :

                                                  The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup generated by the image of the set.

                                                  def AddHom.restrict {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [AddMemClass σ M] (f : AddHom M N) (S : σ) :
                                                  AddHom (↥S) N

                                                  Restriction of an AddSemigroup hom to an AddSubsemigroup of the domain.

                                                  Equations
                                                  Instances For
                                                    def MulHom.restrict {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) (S : σ) :
                                                    S →ₙ* N

                                                    Restriction of a semigroup hom to a subsemigroup of the domain.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem AddHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [AddMemClass σ M] (f : AddHom M N) {S : σ} (x : S) :
                                                      (f.restrict S) x = f x
                                                      @[simp]
                                                      theorem MulHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : S) :
                                                      (f.restrict S) x = f x
                                                      theorem AddHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} {σ : Type u_2} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (x : M) (y : M) :
                                                      (fun (n : M) => f n, ) (x + y) = (fun (n : M) => f n, ) x + (fun (n : M) => f n, ) y
                                                      def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) :
                                                      AddHom M S

                                                      Restriction of an AddSemigroup hom to an AddSubsemigroup of the codomain.

                                                      Equations
                                                      • f.codRestrict S h = { toFun := fun (n : M) => f n, , map_add' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem MulHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
                                                        ((f.codRestrict S h) n) = f n
                                                        @[simp]
                                                        theorem AddHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
                                                        ((f.codRestrict S h) n) = f n
                                                        def MulHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) :
                                                        M →ₙ* S

                                                        Restriction of a semigroup hom to a subsemigroup of the codomain.

                                                        Equations
                                                        • f.codRestrict S h = { toFun := fun (n : M) => f n, , map_mul' := }
                                                        Instances For
                                                          theorem AddHom.srangeRestrict.proof_1 {M : Type u_1} [Add M] {N : Type u_2} [Add N] (f : AddHom M N) (x : M) :
                                                          ∃ (y : M), f y = f x
                                                          def AddHom.srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) :
                                                          AddHom M f.srange

                                                          Restriction of an AddSemigroup hom to its range interpreted as a subsemigroup.

                                                          Equations
                                                          • f.srangeRestrict = f.codRestrict f.srange
                                                          Instances For
                                                            def MulHom.srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) :
                                                            M →ₙ* f.srange

                                                            Restriction of a semigroup hom to its range interpreted as a subsemigroup.

                                                            Equations
                                                            • f.srangeRestrict = f.codRestrict f.srange
                                                            Instances For
                                                              @[simp]
                                                              theorem AddHom.coe_srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (x : M) :
                                                              (f.srangeRestrict x) = f x
                                                              @[simp]
                                                              theorem MulHom.coe_srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (x : M) :
                                                              (f.srangeRestrict x) = f x
                                                              theorem AddHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                                                              Function.Surjective f.srangeRestrict
                                                              theorem MulHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                              Function.Surjective f.srangeRestrict
                                                              theorem AddHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [Add M] [Add N] {M' : Type u_5} {N' : Type u_6} [Add M'] [Add N'] (f : AddHom M N) (g : AddHom M' N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N') :
                                                              AddSubsemigroup.comap (f.prodMap g) (S.prod S') = (AddSubsemigroup.comap f S).prod (AddSubsemigroup.comap g S')
                                                              theorem MulHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {M' : Type u_5} {N' : Type u_6} [Mul M'] [Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup N') :
                                                              Subsemigroup.comap (f.prodMap g) (S.prod S') = (Subsemigroup.comap f S).prod (Subsemigroup.comap g S')
                                                              theorem AddHom.subsemigroupComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : (AddSubsemigroup.comap f N')) :
                                                              def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) :

                                                              The AddHom from the preimage of an additive subsemigroup to itself.

                                                              Equations
                                                              • f.subsemigroupComap N' = { toFun := fun (x : (AddSubsemigroup.comap f N')) => f x, , map_add' := }
                                                              Instances For
                                                                theorem AddHom.subsemigroupComap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : (AddSubsemigroup.comap f N')) (y : (AddSubsemigroup.comap f N')) :
                                                                (fun (x : (AddSubsemigroup.comap f N')) => f x, ) (x + y) = (fun (x : (AddSubsemigroup.comap f N')) => f x, ) x + (fun (x : (AddSubsemigroup.comap f N')) => f x, ) y
                                                                @[simp]
                                                                theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : (AddSubsemigroup.comap f N')) :
                                                                ((f.subsemigroupComap N') x) = f x
                                                                @[simp]
                                                                theorem MulHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) (x : (Subsemigroup.comap f N')) :
                                                                ((f.subsemigroupComap N') x) = f x
                                                                def MulHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) :
                                                                (Subsemigroup.comap f N') →ₙ* N'

                                                                The MulHom from the preimage of a subsemigroup to itself.

                                                                Equations
                                                                • f.subsemigroupComap N' = { toFun := fun (x : (Subsemigroup.comap f N')) => f x, , map_mul' := }
                                                                Instances For
                                                                  def AddHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
                                                                  AddHom M' (AddSubsemigroup.map f M')

                                                                  the AddHom from an additive subsemigroup to its image. See AddEquiv.addSubsemigroupMap for a variant for AddEquivs.

                                                                  Equations
                                                                  • f.subsemigroupMap M' = { toFun := fun (x : M') => f x, , map_add' := }
                                                                  Instances For
                                                                    theorem AddHom.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : M') (y : M') :
                                                                    (fun (x : M') => f x, ) (x + y) = (fun (x : M') => f x, ) x + (fun (x : M') => f x, ) y
                                                                    theorem AddHom.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : M') :
                                                                    aM', f a = f x
                                                                    @[simp]
                                                                    theorem MulHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) (x : M') :
                                                                    ((f.subsemigroupMap M') x) = f x
                                                                    @[simp]
                                                                    theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : M') :
                                                                    ((f.subsemigroupMap M') x) = f x
                                                                    def MulHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :
                                                                    M' →ₙ* (Subsemigroup.map f M')

                                                                    The MulHom from a subsemigroup to its image. See MulEquiv.subsemigroupMap for a variant for MulEquivs.

                                                                    Equations
                                                                    • f.subsemigroupMap M' = { toFun := fun (x : M') => f x, , map_mul' := }
                                                                    Instances For
                                                                      theorem AddHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
                                                                      Function.Surjective (f.subsemigroupMap M')
                                                                      theorem MulHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :
                                                                      Function.Surjective (f.subsemigroupMap M')
                                                                      @[simp]
                                                                      theorem AddSubsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty N] :
                                                                      (AddHom.fst M N).srange =
                                                                      @[simp]
                                                                      theorem Subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty N] :
                                                                      (MulHom.fst M N).srange =
                                                                      @[simp]
                                                                      theorem AddSubsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] :
                                                                      (AddHom.snd M N).srange =
                                                                      @[simp]
                                                                      theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] :
                                                                      (MulHom.snd M N).srange =
                                                                      theorem AddSubsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] [Nonempty N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} :
                                                                      s.prod t = s = t =
                                                                      theorem Subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :
                                                                      s.prod t = s = t =
                                                                      theorem AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) (x : S) :
                                                                      def AddSubsemigroup.inclusion {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) :
                                                                      AddHom S T

                                                                      The AddSemigroup hom associated to an inclusion of subsemigroups.

                                                                      Equations
                                                                      Instances For
                                                                        def Subsemigroup.inclusion {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S T) :
                                                                        S →ₙ* T

                                                                        The semigroup hom associated to an inclusion of subsemigroups.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem AddSubsemigroup.range_subtype {M : Type u_1} [Add M] (s : AddSubsemigroup M) :
                                                                          (AddMemClass.subtype s).srange = s
                                                                          @[simp]
                                                                          theorem Subsemigroup.range_subtype {M : Type u_1} [Mul M] (s : Subsemigroup M) :
                                                                          (MulMemClass.subtype s).srange = s
                                                                          theorem AddSubsemigroup.eq_top_iff' {M : Type u_1} [Add M] (S : AddSubsemigroup M) :
                                                                          S = ∀ (x : M), x S
                                                                          theorem Subsemigroup.eq_top_iff' {M : Type u_1} [Mul M] (S : Subsemigroup M) :
                                                                          S = ∀ (x : M), x S
                                                                          def AddEquiv.subsemigroupCongr {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                          S ≃+ T

                                                                          Makes the identity additive isomorphism from a proof two subsemigroups of an additive semigroup are equal.

                                                                          Equations
                                                                          Instances For
                                                                            theorem AddEquiv.subsemigroupCongr.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                            S = T
                                                                            theorem AddEquiv.subsemigroupCongr.proof_2 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                            ∀ (x x_1 : S), (Equiv.setCongr ).toFun (x + x_1) = (Equiv.setCongr ).toFun (x + x_1)
                                                                            def MulEquiv.subsemigroupCongr {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S = T) :
                                                                            S ≃* T

                                                                            Makes the identity isomorphism from a proof that two subsemigroups of a multiplicative semigroup are equal.

                                                                            Equations
                                                                            Instances For
                                                                              def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) :
                                                                              M ≃+ f.srange

                                                                              An additive semigroup homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.srange. This is a bidirectional version of AddHom.srangeRestrict.

                                                                              Equations
                                                                              Instances For
                                                                                theorem AddEquiv.ofLeftInverse.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) (x : f.srange) :
                                                                                f.srangeRestrict ((g (AddMemClass.subtype f.srange)) x) = x
                                                                                theorem AddEquiv.ofLeftInverse.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (x : M) (y : M) :
                                                                                f.srangeRestrict.toFun (x + y) = f.srangeRestrict.toFun x + f.srangeRestrict.toFun y
                                                                                @[simp]
                                                                                theorem MulEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) :
                                                                                ∀ (a : f.srange), (MulEquiv.ofLeftInverse f h).symm a = g a
                                                                                @[simp]
                                                                                theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
                                                                                (AddEquiv.ofLeftInverse f h) a = f.srangeRestrict a
                                                                                @[simp]
                                                                                theorem MulEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
                                                                                (MulEquiv.ofLeftInverse f h) a = f.srangeRestrict a
                                                                                @[simp]
                                                                                theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) :
                                                                                ∀ (a : f.srange), (AddEquiv.ofLeftInverse f h).symm a = g a
                                                                                def MulEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) :
                                                                                M ≃* f.srange

                                                                                A semigroup homomorphism f : M →ₙ* N with a left-inverse g : N → M defines a multiplicative equivalence between M and f.srange.

                                                                                This is a bidirectional version of MulHom.srangeRestrict.

                                                                                Equations
                                                                                Instances For
                                                                                  theorem AddEquiv.subsemigroupMap.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : (AddSubsemigroup.map (↑e) S)) :
                                                                                  (↑e).symm x S
                                                                                  theorem AddEquiv.subsemigroupMap.proof_5 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                  Function.RightInverse ((↑e).image S).invFun ((↑e).image S).toFun
                                                                                  def AddEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                  S ≃+ (AddSubsemigroup.map (↑e) S)

                                                                                  An AddEquiv φ between two additive semigroups M and N induces an AddEquiv between a subsemigroup S ≤ M and the subsemigroup φ(S) ≤ N. See AddHom.addSubsemigroupMap for a variant for AddHoms.

                                                                                  Equations
                                                                                  • e.subsemigroupMap S = { toFun := fun (x : S) => e x, , invFun := fun (x : (AddSubsemigroup.map (↑e) S)) => e.symm x, , left_inv := , right_inv := , map_add' := }
                                                                                  Instances For
                                                                                    theorem AddEquiv.subsemigroupMap.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : S) :
                                                                                    e x e '' S
                                                                                    theorem AddEquiv.subsemigroupMap.proof_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                    Function.LeftInverse ((↑e).image S).invFun ((↑e).image S).toFun
                                                                                    theorem AddEquiv.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                                                                    AddHomClass (M ≃+ N) M N
                                                                                    theorem AddEquiv.subsemigroupMap.proof_6 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : S) (y : S) :
                                                                                    ((↑e).subsemigroupMap S).toFun (x + y) = ((↑e).subsemigroupMap S).toFun x + ((↑e).subsemigroupMap S).toFun y
                                                                                    @[simp]
                                                                                    theorem AddEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : S) :
                                                                                    ((e.subsemigroupMap S) x) = e x
                                                                                    @[simp]
                                                                                    theorem MulEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : (Subsemigroup.map (↑e) S)) :
                                                                                    ((e.subsemigroupMap S).symm x) = e.symm x
                                                                                    @[simp]
                                                                                    theorem AddEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : (AddSubsemigroup.map (↑e) S)) :
                                                                                    ((e.subsemigroupMap S).symm x) = e.symm x
                                                                                    @[simp]
                                                                                    theorem MulEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : S) :
                                                                                    ((e.subsemigroupMap S) x) = e x
                                                                                    def MulEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) :
                                                                                    S ≃* (Subsemigroup.map (↑e) S)

                                                                                    A MulEquiv φ between two semigroups M and N induces a MulEquiv between a subsemigroup S ≤ M and the subsemigroup φ(S) ≤ N. See MulHom.subsemigroupMap for a variant for MulHoms.

                                                                                    Equations
                                                                                    • e.subsemigroupMap S = { toFun := fun (x : S) => e x, , invFun := fun (x : (Subsemigroup.map (↑e) S)) => e.symm x, , left_inv := , right_inv := , map_mul' := }
                                                                                    Instances For
                                                                                      theorem AddSubsemigroup.map_comap_eq {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup N) :
                                                                                      theorem Subsemigroup.map_comap_eq {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup N) :
                                                                                      theorem AddSubsemigroup.map_comap_eq_self {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : AddSubsemigroup N} (h : S f.srange) :
                                                                                      theorem Subsemigroup.map_comap_eq_self {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : Subsemigroup N} (h : S f.srange) :