Documentation

Mathlib.GroupTheory.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
    @[inline, reducible]

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

    Equations
    • AddSubsemigroup.toSubsemigroup' = OrderIso.symm Subsemigroup.toAddSubsemigroup
    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 (Multiplicative.ofAdd ⁻¹' 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
        @[inline, reducible]

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

        Equations
        • Subsemigroup.toAddSubsemigroup' = OrderIso.symm AddSubsemigroup.toSubsemigroup
        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 (Additive.ofMul ⁻¹' 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} :
              x Subsemigroup.comap f S f x S
              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 x, x S 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 x, x S 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 : { x // x S }) :
                  f x AddSubsemigroup.map f 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 : { x // x S }) :
                  f x Subsemigroup.map f 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} :
                  f x Subsemigroup.map f S x S
                  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 (_ : a, a S ↑(AddHom.id M) a = x)) → motive x_1
                  Equations
                  • One or more equations did not get rendered due to their size.
                  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
                    • One or more equations did not get rendered due to their size.
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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, f a = x) → Prop) :
                        (x : a, f a = x) → ((y : M) → (hy : f y = x) → motive (_ : a, f a = x)) → motive x
                        Equations
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          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
                            • One or more equations did not get rendered due to their size.
                            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
                              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 : { x // x S' }) (b : { x // x S' }) :
                              a + b S'
                              instance AddMemClass.add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
                              Add { x // x S' }

                              An additive submagma of an additive magma inherits an addition.

                              Equations
                              instance MulMemClass.mul {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
                              Mul { x // x 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 : { x // x S' }) (y : { x // x 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 : { x // x S' }) (y : { x // x 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') :
                              { val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := (_ : x + y S') }
                              @[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') :
                              { val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := (_ : x * y S') }
                              theorem AddMemClass.add_def {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
                              x + y = { val := x + y, property := (_ : x + y S') }
                              theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
                              x * y = { val := x * y, property := (_ : x * y S') }
                              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 : { x // x 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) :
                              AddSemigroup { x // x S }

                              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 => a
                              instance MulMemClass.toSemigroup {M : Type u_6} [Semigroup M] {A : Type u_7} [SetLike A M] [MulMemClass A M] (S : A) :
                              Semigroup { x // x S }

                              A subsemigroup of a semigroup inherits a semigroup structure.

                              Equations
                              instance AddMemClass.toAddCommSemigroup {M : Type u_7} [AddCommSemigroup M] {A : Type u_6} [SetLike A M] [AddMemClass A M] (S : A) :
                              AddCommSemigroup { x // x S }

                              An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

                              Equations
                              theorem AddMemClass.toAddCommSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun a => 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 : { x // x 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) :
                              CommSemigroup { x // x S }

                              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 : { x // x 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 { x // x 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) :
                                { x // x 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_2 {M : Type u_1} [Add M] :
                                  ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)
                                  def AddSubsemigroup.topEquiv {M : Type u_1} [Add M] :
                                  { x // x } ≃+ M

                                  The top additive subsemigroup is isomorphic to the additive semigroup.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem AddSubsemigroup.topEquiv.proof_3 {M : Type u_1} [Add M] :
                                    ∀ (x x_1 : { x // x }), Equiv.toFun { toFun := fun x => x, invFun := fun x => { val := x, property := (_ : x ) }, left_inv := (_ : ∀ (x : { x // x }), { val := x, property := (_ : (fun x => x) x ) } = x), right_inv := (_ : ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)) } (x + x_1) = Equiv.toFun { toFun := fun x => x, invFun := fun x => { val := x, property := (_ : x ) }, left_inv := (_ : ∀ (x : { x // x }), { val := x, property := (_ : (fun x => x) x ) } = x), right_inv := (_ : ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)) } (x + x_1)
                                    theorem AddSubsemigroup.topEquiv.proof_1 {M : Type u_1} [Add M] (x : { x // x }) :
                                    { val := x, property := (_ : (fun x => x) x ) } = x
                                    @[simp]
                                    theorem Subsemigroup.topEquiv_apply {M : Type u_1} [Mul M] (x : { x // x }) :
                                    Subsemigroup.topEquiv x = x
                                    @[simp]
                                    theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Mul M] (x : M) :
                                    ↑(↑(MulEquiv.symm Subsemigroup.topEquiv) x) = x
                                    @[simp]
                                    theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [Add M] (x : { x // x }) :
                                    AddSubsemigroup.topEquiv x = x
                                    @[simp]
                                    theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Add M] (x : M) :
                                    ↑(↑(AddEquiv.symm AddSubsemigroup.topEquiv) x) = x
                                    def Subsemigroup.topEquiv {M : Type u_1} [Mul M] :
                                    { x // x } ≃* M

                                    The top subsemigroup is isomorphic to the semigroup.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    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_3 {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 : { x // x S }), Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } x + Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } x_1
                                      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) :
                                      Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
                                      theorem AddSubsemigroup.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
                                      Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
                                      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) :
                                      { x // x S } ≃+ { x // x AddSubsemigroup.map f S }

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      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) :
                                        { x // x S } ≃* { x // x Subsemigroup.map f S }

                                        A subsemigroup is isomorphic to its image under an injective function

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        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 : { x // x S }) :
                                          ↑(↑(AddSubsemigroup.equivMapOfInjective S 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 : { x // x S }) :
                                          ↑(↑(Subsemigroup.equivMapOfInjective S 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
                                          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).fst s (a + b).snd 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
                                            Instances For
                                              theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                              ↑(AddSubsemigroup.prod s 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) :
                                              ↑(Subsemigroup.prod s 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 AddSubsemigroup.prod s t p.fst s p.snd 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 Subsemigroup.prod s t p.fst s p.snd 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₂) :
                                              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₂) :
                                              @[simp]
                                              @[simp]
                                              theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
                                              theorem AddSubsemigroup.prodEquiv.proof_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                              ∀ (x x_1 : { x // x AddSubsemigroup.prod s t }), Equiv.toFun { toFun := (Equiv.Set.prod s t).toFun, invFun := (Equiv.Set.prod s t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.prod s t).toFun, invFun := (Equiv.Set.prod s t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun) } (x + x_1)
                                              theorem AddSubsemigroup.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                              Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
                                              def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                              { x // x AddSubsemigroup.prod s t } ≃+ { x // x s } × { x // x t }

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

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem AddSubsemigroup.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
                                                theorem AddSubsemigroup.prodEquiv.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
                                                Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
                                                def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
                                                { x // x Subsemigroup.prod s t } ≃* { x // x s } × { x // x t }

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                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} :
                                                  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 ↑(MulEquiv.symm f) x K
                                                  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) :
                                                  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) :
                                                  @[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) :
                                                  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) :
                                                      @[simp]
                                                      theorem MulHom.coe_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                      @[simp]
                                                      theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {y : N} :
                                                      y AddHom.srange f x, 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 MulHom.srange f x, 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) :
                                                      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) :
                                                      @[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) :

                                                      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) :

                                                      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 { x // x 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 : σ) :
                                                        { x // x 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 : { x // x S }) :
                                                          ↑(AddHom.restrict f 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 : { x // x S }) :
                                                          ↑(MulHom.restrict f 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 => { val := f n, property := h n }) (x + y) = (fun n => { val := f n, property := h n }) x + (fun n => { val := f n, property := h 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 { x // x S }

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

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          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) :
                                                            ↑(↑(MulHom.codRestrict f 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) :
                                                            ↑(↑(AddHom.codRestrict f 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 →ₙ* { x // x S }

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

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            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, 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 { x // x AddHom.srange f }

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

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

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

                                                                Equations
                                                                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) :
                                                                  ↑(↑(AddHom.srangeRestrict f) 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) :
                                                                  ↑(↑(MulHom.srangeRestrict f) 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 : { x // x AddHom.srange f }Prop) :
                                                                  (x : { x // x AddHom.srange f }) → ((x : M) → motive { val := f x, property := (_ : y, f y = f x) }) → motive x
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    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') :
                                                                    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') :
                                                                    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 : { x // x AddSubsemigroup.comap f N' }) :
                                                                    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 : { x // x AddSubsemigroup.comap f N' }) (y : { x // x AddSubsemigroup.comap f N' }) :
                                                                    (fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) (x + y) = (fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) x + (fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) y
                                                                    def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) :
                                                                    AddHom { x // x AddSubsemigroup.comap f N' } { x // x N' }

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

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[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 : { x // x AddSubsemigroup.comap f N' }) :
                                                                      ↑(↑(AddHom.subsemigroupComap f 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 : { x // x Subsemigroup.comap f N' }) :
                                                                      ↑(↑(MulHom.subsemigroupComap f 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) :
                                                                      { x // x Subsemigroup.comap f N' } →ₙ* { x // x N' }

                                                                      The MulHom from the preimage of a subsemigroup to itself.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      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 : { x // x M' }) :
                                                                        a, a M' 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 : { x // x M' }) (y : { x // x M' }) :
                                                                        (fun x => { val := f x, property := (_ : a, a M' f a = f x) }) (x + y) = (fun x => { val := f x, property := (_ : a, a M' f a = f x) }) x + (fun x => { val := f x, property := (_ : a, a M' f a = 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 { x // x M' } { x // x AddSubsemigroup.map f M' }

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

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[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 : { x // x M' }) :
                                                                          ↑(↑(AddHom.subsemigroupMap f M') x) = 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 : { x // x M' }) :
                                                                          ↑(↑(MulHom.subsemigroupMap f 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) :
                                                                          { x // x M' } →ₙ* { x // x Subsemigroup.map f M' }

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

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem AddSubsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty N] :
                                                                            @[simp]
                                                                            theorem Subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty N] :
                                                                            @[simp]
                                                                            theorem AddSubsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] :
                                                                            @[simp]
                                                                            theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] :
                                                                            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} :
                                                                            theorem AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) (x : { x // x S }) :
                                                                            def AddSubsemigroup.inclusion {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) :
                                                                            AddHom { x // x S } { x // x 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) :
                                                                              { x // x S } →ₙ* { x // x T }

                                                                              The semigroup hom associated to an inclusion of subsemigroups.

                                                                              Equations
                                                                              Instances For
                                                                                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
                                                                                theorem AddEquiv.subsemigroupCongr.proof_4 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                                ∀ (x x_1 : { x // x S }), Equiv.toFun { toFun := (Equiv.setCongr (_ : S = T)).toFun, invFun := (Equiv.setCongr (_ : S = T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.setCongr (_ : S = T)).toFun, invFun := (Equiv.setCongr (_ : S = T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun) } (x + x_1)
                                                                                def AddEquiv.subsemigroupCongr {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                                { x // x S } ≃+ { x // x T }

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

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                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_3 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                                  Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun
                                                                                  theorem AddEquiv.subsemigroupCongr.proof_2 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
                                                                                  Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun
                                                                                  def MulEquiv.subsemigroupCongr {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S = T) :
                                                                                  { x // x S } ≃* { x // x T }

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

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  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 : { x // x AddHom.srange f }) :
                                                                                    abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : { x // x AddHom.srange f }) (motive : (x, f x = x) → Prop) :
                                                                                    (x : x, f x = x) → ((x' : M) → (hx' : f x' = x) → motive (_ : x, f x = x)) → motive x
                                                                                    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 ≃+ { x // x AddHom.srange f }

                                                                                      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
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[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 : { x // x MulHom.srange f }), ↑(MulEquiv.symm (MulEquiv.ofLeftInverse f h)) 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) :
                                                                                        @[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) :
                                                                                        @[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 : { x // x AddHom.srange f }), ↑(AddEquiv.symm (AddEquiv.ofLeftInverse f h)) 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 ≃* { x // x MulHom.srange f }

                                                                                        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
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def AddEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                          { x // x S } ≃+ { x // x 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_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                            Function.RightInverse (Equiv.image e S).invFun (Equiv.image e S).toFun
                                                                                            theorem AddEquiv.subsemigroupMap.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x S }) :
                                                                                            e x e '' S
                                                                                            theorem AddEquiv.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // 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) (x : { x // x S }) (y : { x // x S }) :
                                                                                            theorem AddEquiv.subsemigroupMap.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
                                                                                            Function.LeftInverse (Equiv.image e S).invFun (Equiv.image e S).toFun
                                                                                            @[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 : { x // x Subsemigroup.map (e) S }) :
                                                                                            @[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 : { x // x AddSubsemigroup.map (e) S }) :
                                                                                            @[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 : { x // x S }) :
                                                                                            ↑(↑(AddEquiv.subsemigroupMap e S) x) = e 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 : { x // x S }) :
                                                                                            ↑(↑(MulEquiv.subsemigroupMap e 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) :
                                                                                            { x // x S } ≃* { x // x 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