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_apply_coe {M : Type u_1} [Mul M] (S : Subsemigroup M) :
(Subsemigroup.toAddSubsemigroup S) = Additive.toMul ⁻¹' S
@[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

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_apply_coe {A : Type u_5} [Add A] (S : AddSubsemigroup A) :
      (AddSubsemigroup.toSubsemigroup S) = Multiplicative.toAdd ⁻¹' 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

      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 #

          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 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
            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]
              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 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
                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.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) :
                  abbrev AddSubsemigroup.map_id.match_1 {M : Type u_1} [Add M] (S : AddSubsemigroup M) :
                  ∀ (x : M) (motive : x AddSubsemigroup.map (AddHom.id M) SProp) (x_1 : x AddSubsemigroup.map (AddHom.id M) S), (∀ (h : x S), motive )motive x_1
                  Equations
                  • =
                  Instances For
                    @[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} :
                        abbrev AddSubsemigroup.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (x : N) (motive : (∃ (a : M), f a = x)Prop) :
                        ∀ (x_1 : ∃ (a : M), f a = x), (∀ (y : M) (hy : f y = x), motive )motive x_1
                        Equations
                        • =
                        Instances For
                          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)
                              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 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
                              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
                              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
                                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 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
                                  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)
                                  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)
                                  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_1 {M : Type u_1} [Add M] (x : ) :
                                    x, = x
                                    @[simp]
                                    theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Mul M] (x : M) :
                                    (Subsemigroup.topEquiv.symm x) = x
                                    @[simp]
                                    theorem Subsemigroup.topEquiv_apply {M : Type u_1} [Mul M] (x : ) :
                                    Subsemigroup.topEquiv x = x
                                    @[simp]
                                    theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [Add M] (x : ) :
                                    AddSubsemigroup.topEquiv x = x
                                    @[simp]
                                    theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Add M] (x : M) :
                                    (AddSubsemigroup.topEquiv.symm 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 = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, 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 = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, 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} :
                                          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 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
                                            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 =
                                              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
                                              • s.prodEquiv t = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_add' := }
                                              Instances For
                                                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)
                                                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
                                                • s.prodEquiv t = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_mul' := }
                                                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)} :
                                                  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 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
                                                    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
                                                      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
                                                              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
                                                                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 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
                                                                  abbrev AddHom.srangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (motive : f.srangeProp) :
                                                                  ∀ (x : f.srange), (∀ (x : M), motive f x, )motive x
                                                                  Equations
                                                                  • =
                                                                  Instances For
                                                                    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_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
                                                                    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_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')) :
                                                                      @[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
                                                                        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
                                                                        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
                                                                        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
                                                                          @[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 =
                                                                            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
                                                                              theorem AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) (x : S) :
                                                                              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_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)
                                                                                  theorem AddEquiv.subsemigroupCongr.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                                  S = T
                                                                                  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
                                                                                    abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : f.srange) (motive : (∃ (x_1 : M), f x_1 = x)Prop) :
                                                                                    ∀ (x_1 : ∃ (x_1 : M), f x_1 = x), (∀ (x' : M) (hx' : f x' = x), motive )motive x_1
                                                                                    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_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
                                                                                        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
                                                                                        @[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_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_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
                                                                                        @[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
                                                                                        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_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                                                                          AddHomClass (M ≃+ N) M N
                                                                                          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
                                                                                          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
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            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
                                                                                            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_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_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 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
                                                                                            @[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_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 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
                                                                                            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
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For