Documentation

Mathlib.GroupTheory.Submonoid.Operations

Operations on Submonoids #

In this file we define various operations on Submonoids and MonoidHoms.

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) monoid structure on a submonoid #

Group actions by submonoids #

Operations on submonoids #

Monoid homomorphisms between submonoid #

Operations on MonoidHoms #

Tags #

submonoid, range, product, map, comap

Conversion to/from Additive/Multiplicative #

@[simp]
theorem Submonoid.toAddSubmonoid_apply_coe {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
↑(Submonoid.toAddSubmonoid S) = Additive.toMul ⁻¹' S
@[simp]
theorem Submonoid.toAddSubmonoid_symm_apply_coe {M : Type u_1} [MulOneClass M] (S : AddSubmonoid (Additive M)) :
↑(↑(RelIso.symm Submonoid.toAddSubmonoid) S) = Additive.ofMul ⁻¹' S

Submonoids of monoid M are isomorphic to additive submonoids of Additive M.

Instances For
    @[inline, reducible]

    Additive submonoids of an additive monoid Additive M are isomorphic to submonoids of M.

    Instances For
      theorem Submonoid.toAddSubmonoid_closure {M : Type u_1} [MulOneClass M] (S : Set M) :
      Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (Additive.toMul ⁻¹' S)
      theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [MulOneClass M] (S : Set (Additive M)) :
      AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (Multiplicative.ofAdd ⁻¹' S)
      @[simp]
      theorem AddSubmonoid.toSubmonoid_apply_coe {A : Type u_4} [AddZeroClass A] (S : AddSubmonoid A) :
      ↑(AddSubmonoid.toSubmonoid S) = Multiplicative.toAdd ⁻¹' S
      @[simp]
      theorem AddSubmonoid.toSubmonoid_symm_apply_coe {A : Type u_4} [AddZeroClass A] (S : Submonoid (Multiplicative A)) :
      ↑(↑(RelIso.symm AddSubmonoid.toSubmonoid) S) = Multiplicative.ofAdd ⁻¹' S

      Additive submonoids of an additive monoid A are isomorphic to multiplicative submonoids of Multiplicative A.

      Instances For
        @[inline, reducible]

        Submonoids of a monoid Multiplicative A are isomorphic to additive submonoids of A.

        Instances For
          theorem AddSubmonoid.toSubmonoid_closure {A : Type u_4} [AddZeroClass A] (S : Set A) :
          AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (Multiplicative.toAdd ⁻¹' S)
          theorem Submonoid.toAddSubmonoid'_closure {A : Type u_4} [AddZeroClass A] (S : Set (Multiplicative A)) :
          Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (Additive.ofMul ⁻¹' S)

          comap and map #

          theorem AddSubmonoid.comap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :
          f 0 S
          theorem AddSubmonoid.comap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :
          ∀ {a b : M}, a f ⁻¹' Sb f ⁻¹' Sf (a + b) S
          def AddSubmonoid.comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

          The preimage of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

          Instances For
            def Submonoid.comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N) :

            The preimage of a submonoid along a monoid homomorphism is a submonoid.

            Instances For
              @[simp]
              theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F) :
              ↑(AddSubmonoid.comap f S) = f ⁻¹' S
              @[simp]
              theorem Submonoid.coe_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F) :
              ↑(Submonoid.comap f S) = f ⁻¹' S
              @[simp]
              theorem AddSubmonoid.mem_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M} :
              x AddSubmonoid.comap f S f x S
              @[simp]
              theorem Submonoid.mem_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M} :
              x Submonoid.comap f S f x S
              theorem Submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (S : Submonoid P) (g : N →* P) (f : M →* N) :
              @[simp]
              theorem AddSubmonoid.map.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :
              ∀ {a b : N}, a f '' Sb f '' Sa + b f '' S
              def AddSubmonoid.map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

              The image of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

              Instances For
                theorem AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :
                a, a S f a = 0
                def Submonoid.map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

                The image of a submonoid along a monoid homomorphism is a submonoid.

                Instances For
                  @[simp]
                  theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :
                  ↑(AddSubmonoid.map f S) = f '' S
                  @[simp]
                  theorem Submonoid.coe_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :
                  ↑(Submonoid.map f S) = f '' S
                  @[simp]
                  theorem AddSubmonoid.mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N} :
                  y AddSubmonoid.map f S x, x S f x = y
                  @[simp]
                  theorem Submonoid.mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N} :
                  y Submonoid.map f S x, x S f x = y
                  theorem AddSubmonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M} (hx : x S) :
                  theorem Submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M} (hx : x S) :
                  f x Submonoid.map f S
                  theorem AddSubmonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x S }) :
                  f x AddSubmonoid.map f S
                  theorem Submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : { x // x S }) :
                  f x Submonoid.map f S
                  theorem AddSubmonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N) :
                  theorem Submonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (S : Submonoid M) (g : N →* P) (f : M →* N) :
                  @[simp]
                  theorem AddSubmonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : AddSubmonoid M} {x : M} :
                  f x AddSubmonoid.map f S x S
                  @[simp]
                  theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : Submonoid M} {x : M} :
                  f x Submonoid.map f S x S
                  theorem AddSubmonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N} :
                  theorem Submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N} :
                  theorem Submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) :
                  theorem AddSubmonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :
                  theorem Submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :
                  theorem AddSubmonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :
                  theorem Submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :
                  theorem AddSubmonoid.le_comap_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} :
                  theorem Submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} :
                  theorem AddSubmonoid.map_comap_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} :
                  theorem Submonoid.map_comap_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :
                  theorem AddSubmonoid.monotone_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} :
                  theorem Submonoid.monotone_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} :
                  theorem AddSubmonoid.monotone_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} :
                  theorem Submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} :
                  @[simp]
                  @[simp]
                  theorem Submonoid.map_comap_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} :
                  @[simp]
                  theorem Submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :
                  theorem AddSubmonoid.map_sup {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid M) (T : AddSubmonoid M) (f : F) :
                  theorem Submonoid.map_sup {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (S : Submonoid M) (T : Submonoid M) (f : F) :
                  theorem AddSubmonoid.map_iSup {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ιAddSubmonoid M) :
                  AddSubmonoid.map f (iSup s) = ⨆ (i : ι), AddSubmonoid.map f (s i)
                  theorem Submonoid.map_iSup {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ιSubmonoid M) :
                  Submonoid.map f (iSup s) = ⨆ (i : ι), Submonoid.map f (s i)
                  theorem AddSubmonoid.comap_inf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (T : AddSubmonoid N) (f : F) :
                  theorem Submonoid.comap_inf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (S : Submonoid N) (T : Submonoid N) (f : F) :
                  theorem AddSubmonoid.comap_iInf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ιAddSubmonoid N) :
                  AddSubmonoid.comap f (iInf s) = ⨅ (i : ι), AddSubmonoid.comap f (s i)
                  theorem Submonoid.comap_iInf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ιSubmonoid N) :
                  Submonoid.comap f (iInf s) = ⨅ (i : ι), Submonoid.comap f (s i)
                  @[simp]
                  theorem AddSubmonoid.map_bot {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) :
                  @[simp]
                  theorem Submonoid.map_bot {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) :
                  @[simp]
                  theorem AddSubmonoid.comap_top {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) :
                  @[simp]
                  theorem Submonoid.comap_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) :
                  abbrev AddSubmonoid.map_id.match_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                  (x : M) → ∀ (motive : x AddSubmonoid.map (AddMonoidHom.id M) SProp) (x_1 : x AddSubmonoid.map (AddMonoidHom.id M) S), (∀ (h : x S), motive (_ : a, a S ↑(AddMonoidHom.id M) a = x)) → motive x_1
                  Instances For
                    @[simp]
                    theorem Submonoid.map_id {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                    theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : AddSubmonoid M) (x : M) :

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

                    Instances For
                      def Submonoid.gciMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :

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

                      Instances For
                        theorem AddSubmonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : AddSubmonoid M) :
                        theorem Submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : Submonoid M) :
                        theorem Submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :
                        theorem Submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : Submonoid M) (T : Submonoid M) :
                        theorem AddSubmonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective f) (S : ιAddSubmonoid M) :
                        AddSubmonoid.comap f (⨅ (i : ι), AddSubmonoid.map f (S i)) = iInf S
                        theorem Submonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective f) (S : ιSubmonoid M) :
                        Submonoid.comap f (⨅ (i : ι), Submonoid.map f (S i)) = iInf S
                        theorem Submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : Submonoid M) (T : Submonoid M) :
                        theorem AddSubmonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective f) (S : ιAddSubmonoid M) :
                        AddSubmonoid.comap f (⨆ (i : ι), AddSubmonoid.map f (S i)) = iSup S
                        theorem Submonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective f) (S : ιSubmonoid M) :
                        Submonoid.comap f (⨆ (i : ι), Submonoid.map f (S i)) = iSup S
                        theorem AddSubmonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : AddSubmonoid M} {T : AddSubmonoid M} :
                        theorem Submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : Submonoid M} {T : Submonoid M} :
                        theorem Submonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :

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

                        Instances For
                          abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (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
                          Instances For
                            theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : AddSubmonoid N) (x : N) (h : x S) :
                            def Submonoid.giMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :

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

                            Instances For
                              theorem Submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : Submonoid N) :
                              theorem Submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : Submonoid N) (T : Submonoid N) :
                              theorem AddSubmonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective f) (S : ιAddSubmonoid N) :
                              AddSubmonoid.map f (⨅ (i : ι), AddSubmonoid.comap f (S i)) = iInf S
                              theorem Submonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective f) (S : ιSubmonoid N) :
                              Submonoid.map f (⨅ (i : ι), Submonoid.comap f (S i)) = iInf S
                              theorem Submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : Submonoid N) (T : Submonoid N) :
                              theorem AddSubmonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective f) (S : ιAddSubmonoid N) :
                              AddSubmonoid.map f (⨆ (i : ι), AddSubmonoid.comap f (S i)) = iSup S
                              theorem Submonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective f) (S : ιSubmonoid N) :
                              Submonoid.map f (⨆ (i : ι), Submonoid.comap f (S i)) = iSup S
                              theorem Submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) {S : Submonoid N} {T : Submonoid N} :
                              theorem Submonoid.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :
                              instance ZeroMemClass.zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
                              Zero { x // x S' }

                              An AddSubmonoid of an AddMonoid inherits a zero.

                              instance OneMemClass.one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
                              One { x // x S' }

                              A submonoid of a monoid inherits a 1.

                              @[simp]
                              theorem ZeroMemClass.coe_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
                              0 = 0
                              @[simp]
                              theorem OneMemClass.coe_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
                              1 = 1
                              @[simp]
                              theorem ZeroMemClass.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : { x // x S' }} :
                              x = 0 x = 0
                              @[simp]
                              theorem OneMemClass.coe_eq_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] {S' : A} {x : { x // x S' }} :
                              x = 1 x = 1
                              theorem ZeroMemClass.zero_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :
                              0 = { val := 0, property := (_ : 0 S') }
                              theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
                              1 = { val := 1, property := (_ : 1 S') }
                              instance AddSubmonoidClass.nSMul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              SMul { x // x S }

                              An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

                              instance SubmonoidClass.nPow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              Pow { x // x S }

                              A submonoid of a monoid inherits a power operator.

                              @[simp]
                              theorem AddSubmonoidClass.coe_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : { x // x S }) (n : ) :
                              ↑(n x) = n x
                              @[simp]
                              theorem SubmonoidClass.coe_pow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] {S : A} (x : { x // x S }) (n : ) :
                              ↑(x ^ n) = x ^ n
                              @[simp]
                              theorem AddSubmonoidClass.mk_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : M) (hx : x S) (n : ) :
                              n { val := x, property := hx } = { val := n x, property := (_ : n x S) }
                              @[simp]
                              theorem SubmonoidClass.mk_pow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x S) (n : ) :
                              { val := x, property := hx } ^ n = { val := x ^ n, property := (_ : x ^ n S) }
                              theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun a => a
                              theorem AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              0 = 0
                              instance AddSubmonoidClass.toAddZeroClass {M : Type u_5} [AddZeroClass M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              AddZeroClass { x // x S }

                              An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

                              theorem AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              instance SubmonoidClass.toMulOneClass {M : Type u_5} [MulOneClass M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              MulOneClass { x // x S }

                              A submonoid of a unital magma inherits a unital magma structure.

                              theorem AddSubmonoidClass.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              0 = 0
                              theorem AddSubmonoidClass.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              theorem AddSubmonoidClass.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun a => a
                              instance AddSubmonoidClass.toAddMonoid {M : Type u_5} [AddMonoid M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              AddMonoid { x // x S }

                              An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

                              instance SubmonoidClass.toMonoid {M : Type u_5} [Monoid M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              Monoid { x // x S }

                              A submonoid of a monoid inherits a monoid structure.

                              theorem AddSubmonoidClass.toAddCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              0 = 0
                              theorem AddSubmonoidClass.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              theorem AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              instance AddSubmonoidClass.toAddCommMonoid {M : Type u_6} [AddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              AddCommMonoid { x // x S }

                              An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

                              theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun a => a
                              instance SubmonoidClass.toCommMonoid {M : Type u_6} [CommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              CommMonoid { x // x S }

                              A submonoid of a CommMonoid is a CommMonoid.

                              theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun a => a
                              theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              instance SubmonoidClass.toOrderedCommMonoid {M : Type u_6} [OrderedCommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              OrderedCommMonoid { x // x S }

                              A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

                              theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                              theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                              theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                              theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                              theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) :
                              ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                              theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                              theorem AddSubmonoidClass.subtype.proof_1 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :
                              0 = 0
                              def AddSubmonoidClass.subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :
                              { x // x S' } →+ M

                              The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

                              Instances For
                                theorem AddSubmonoidClass.subtype.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] (S' : A) :
                                ∀ (x x_1 : { x // x S' }), x + x_1 = x + x_1
                                def SubmonoidClass.subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [SetLike A M] [hA : SubmonoidClass A M] (S' : A) :
                                { x // x S' } →* M

                                The natural monoid hom from a submonoid of monoid M to M.

                                Instances For
                                  @[simp]
                                  theorem AddSubmonoidClass.coe_subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :
                                  ↑(AddSubmonoidClass.subtype S') = Subtype.val
                                  @[simp]
                                  theorem SubmonoidClass.coe_subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [SetLike A M] [hA : SubmonoidClass A M] (S' : A) :
                                  ↑(SubmonoidClass.subtype S') = Subtype.val
                                  instance AddSubmonoid.add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  Add { x // x S }

                                  An AddSubmonoid of an AddMonoid inherits an addition.

                                  theorem AddSubmonoid.add.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (a : { x // x S }) (b : { x // x S }) :
                                  a + b S
                                  instance Submonoid.mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  Mul { x // x S }

                                  A submonoid of a monoid inherits a multiplication.

                                  instance AddSubmonoid.zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  Zero { x // x S }

                                  An AddSubmonoid of an AddMonoid inherits a zero.

                                  instance Submonoid.one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  One { x // x S }

                                  A submonoid of a monoid inherits a 1.

                                  @[simp]
                                  theorem AddSubmonoid.coe_add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : { x // x S }) (y : { x // x S }) :
                                  ↑(x + y) = x + y
                                  @[simp]
                                  theorem Submonoid.coe_mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : { x // x S }) (y : { x // x S }) :
                                  ↑(x * y) = x * y
                                  @[simp]
                                  theorem AddSubmonoid.coe_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  0 = 0
                                  @[simp]
                                  theorem Submonoid.coe_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  1 = 1
                                  @[simp]
                                  theorem AddSubmonoid.mk_add_mk {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (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 Submonoid.mk_mul_mk {M : Type u_1} [MulOneClass M] (S : Submonoid M) (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 AddSubmonoid.add_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : { x // x S }) (y : { x // x S }) :
                                  x + y = { val := x + y, property := (_ : x + y S) }
                                  theorem Submonoid.mul_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : { x // x S }) (y : { x // x S }) :
                                  x * y = { val := x * y, property := (_ : x * y S) }
                                  theorem AddSubmonoid.zero_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  0 = { val := 0, property := (_ : 0 S) }
                                  theorem Submonoid.one_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  1 = { val := 1, property := (_ : 1 S) }
                                  instance AddSubmonoid.toAddZeroClass {M : Type u_5} [AddZeroClass M] (S : AddSubmonoid M) :
                                  AddZeroClass { x // x S }

                                  An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

                                  theorem AddSubmonoid.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  instance Submonoid.toMulOneClass {M : Type u_5} [MulOneClass M] (S : Submonoid M) :
                                  MulOneClass { x // x S }

                                  A submonoid of a unital magma inherits a unital magma structure.

                                  theorem AddSubmonoid.nsmul_mem {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) {x : M} (hx : x S) (n : ) :
                                  n x S
                                  theorem Submonoid.pow_mem {M : Type u_5} [Monoid M] (S : Submonoid M) {x : M} (hx : x S) (n : ) :
                                  x ^ n S
                                  theorem AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  instance AddSubmonoid.toAddMonoid {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) :
                                  AddMonoid { x // x S }

                                  An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

                                  theorem AddSubmonoid.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  0 = 0
                                  instance Submonoid.toMonoid {M : Type u_5} [Monoid M] (S : Submonoid M) :
                                  Monoid { x // x S }

                                  A submonoid of a monoid inherits a monoid structure.

                                  theorem AddSubmonoid.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  theorem AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  instance Submonoid.toCommMonoid {M : Type u_5} [CommMonoid M] (S : Submonoid M) :
                                  CommMonoid { x // x S }

                                  A submonoid of a CommMonoid is a CommMonoid.

                                  theorem AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  theorem AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                                  theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                                  theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                                  theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
                                  theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
                                  theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
                                  theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : { x // x S }), x + x_1 = x + x_1
                                  theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  0 = 0
                                  def AddSubmonoid.subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  { x // x S } →+ M

                                  The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

                                  Instances For
                                    def Submonoid.subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                    { x // x S } →* M

                                    The natural monoid hom from a submonoid of monoid M to M.

                                    Instances For
                                      @[simp]
                                      theorem AddSubmonoid.coe_subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                      ↑(AddSubmonoid.subtype S) = Subtype.val
                                      @[simp]
                                      theorem Submonoid.coe_subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                      ↑(Submonoid.subtype S) = Subtype.val
                                      theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [AddZeroClass M] (x : { x // x }) :
                                      { val := x, property := (_ : (fun x => x) x ) } = x
                                      theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [AddZeroClass 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 AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] :
                                      ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)
                                      def AddSubmonoid.topEquiv {M : Type u_1} [AddZeroClass M] :
                                      { x // x } ≃+ M

                                      The top additive submonoid is isomorphic to the additive monoid.

                                      Instances For
                                        @[simp]
                                        theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_1} [AddZeroClass M] (x : M) :
                                        ↑(↑(AddEquiv.symm AddSubmonoid.topEquiv) x) = x
                                        @[simp]
                                        theorem Submonoid.topEquiv_symm_apply_coe {M : Type u_1} [MulOneClass M] (x : M) :
                                        ↑(↑(MulEquiv.symm Submonoid.topEquiv) x) = x
                                        @[simp]
                                        theorem AddSubmonoid.topEquiv_apply {M : Type u_1} [AddZeroClass M] (x : { x // x }) :
                                        AddSubmonoid.topEquiv x = x
                                        @[simp]
                                        theorem Submonoid.topEquiv_apply {M : Type u_1} [MulOneClass M] (x : { x // x }) :
                                        Submonoid.topEquiv x = x
                                        def Submonoid.topEquiv {M : Type u_1} [MulOneClass M] :
                                        { x // x } ≃* M

                                        The top submonoid is isomorphic to the monoid.

                                        Instances For
                                          noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective f) :
                                          { x // x S } ≃+ { x // x AddSubmonoid.map f S }

                                          An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubmonoidMap for better definitional equalities.

                                          Instances For
                                            theorem AddSubmonoid.equivMapOfInjective.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : 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 AddSubmonoid.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective f) :
                                            Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
                                            theorem AddSubmonoid.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective f) :
                                            Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
                                            noncomputable def Submonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) (hf : Function.Injective f) :
                                            { x // x S } ≃* { x // x Submonoid.map f S }

                                            A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.submonoidMap for better definitional equalities.

                                            Instances For
                                              @[simp]
                                              theorem AddSubmonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective f) (x : { x // x S }) :
                                              ↑(↑(AddSubmonoid.equivMapOfInjective S f hf) x) = f x
                                              @[simp]
                                              theorem Submonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) (hf : Function.Injective f) (x : { x // x S }) :
                                              ↑(↑(Submonoid.equivMapOfInjective S f hf) x) = f x
                                              @[simp]
                                              theorem AddSubmonoid.prod.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                              ∀ {a b : M × N}, a s ×ˢ tb s ×ˢ t(a + b).fst s (a + b).snd t
                                              def AddSubmonoid.prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

                                              Given AddSubmonoids s, t of AddMonoids A, B respectively, s × t as an AddSubmonoid of A × B.

                                              Instances For
                                                theorem AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                0.fst s 0.snd t
                                                def Submonoid.prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) (t : Submonoid N) :

                                                Given submonoids s, t of monoids M, N respectively, s × t as a submonoid of M × N.

                                                Instances For
                                                  theorem AddSubmonoid.coe_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                  ↑(AddSubmonoid.prod s t) = s ×ˢ t
                                                  theorem Submonoid.coe_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) (t : Submonoid N) :
                                                  ↑(Submonoid.prod s t) = s ×ˢ t
                                                  theorem AddSubmonoid.mem_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {p : M × N} :
                                                  p AddSubmonoid.prod s t p.fst s p.snd t
                                                  theorem Submonoid.mem_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {p : M × N} :
                                                  p Submonoid.prod s t p.fst s p.snd t
                                                  theorem AddSubmonoid.prod_mono {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s₁ : AddSubmonoid M} {s₂ : AddSubmonoid M} {t₁ : AddSubmonoid N} {t₂ : AddSubmonoid N} (hs : s₁ s₂) (ht : t₁ t₂) :
                                                  theorem Submonoid.prod_mono {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s₁ : Submonoid M} {s₂ : Submonoid M} {t₁ : Submonoid N} {t₂ : Submonoid N} (hs : s₁ s₂) (ht : t₁ t₂) :
                                                  Submonoid.prod s₁ t₁ Submonoid.prod s₂ t₂
                                                  theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                  Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
                                                  def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                  { x // x AddSubmonoid.prod s t } ≃+ { x // x s } × { x // x t }

                                                  The product of additive submonoids is isomorphic to their product as additive monoids

                                                  Instances For
                                                    theorem AddSubmonoid.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                    Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
                                                    theorem AddSubmonoid.prodEquiv.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                    ∀ (x x_1 : { x // x AddSubmonoid.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)
                                                    def Submonoid.prodEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) (t : Submonoid N) :
                                                    { x // x Submonoid.prod s t } ≃* { x // x s } × { x // x t }

                                                    The product of submonoids is isomorphic to their product as monoids.

                                                    Instances For
                                                      abbrev AddSubmonoid.map_inl.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p AddSubmonoid.map (AddMonoidHom.inl M N) sProp) :
                                                      (x : p AddSubmonoid.map (AddMonoidHom.inl M N) s) → ((w : M) → (hx : w s) → (hp : ↑(AddMonoidHom.inl M N) w = p) → motive (_ : a, a s ↑(AddMonoidHom.inl M N) a = p)) → motive x
                                                      Instances For
                                                        abbrev AddSubmonoid.map_inl.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p AddSubmonoid.prod s Prop) :
                                                        (x : p AddSubmonoid.prod s ) → ((hps : p.fst s) → (hp1 : p.snd ) → motive (_ : p.fst s p.snd )) → motive x
                                                        Instances For
                                                          abbrev AddSubmonoid.map_inr.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p AddSubmonoid.prod sProp) :
                                                          (x : p AddSubmonoid.prod s) → ((hp1 : p.fst ) → (hps : p.snd s) → motive (_ : p.fst p.snd s)) → motive x
                                                          Instances For
                                                            abbrev AddSubmonoid.map_inr.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p AddSubmonoid.map (AddMonoidHom.inr M N) sProp) :
                                                            (x : p AddSubmonoid.map (AddMonoidHom.inr M N) s) → ((w : N) → (hx : w s) → (hp : ↑(AddMonoidHom.inr M N) w = p) → motive (_ : a, a s ↑(AddMonoidHom.inr M N) a = p)) → motive x
                                                            Instances For
                                                              theorem AddSubmonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M ≃+ N} {K : AddSubmonoid M} {x : N} :
                                                              theorem Submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M ≃* N} {K : Submonoid M} {x : N} :
                                                              @[simp]
                                                              theorem AddMonoidHom.mrange.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) :
                                                              Set.range f = f '' Set.univ
                                                              def AddMonoidHom.mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) :

                                                              The range of an AddMonoidHom is an AddSubmonoid.

                                                              Instances For
                                                                def MonoidHom.mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :

                                                                The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].

                                                                Instances For
                                                                  @[simp]
                                                                  theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) :
                                                                  @[simp]
                                                                  theorem MonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :
                                                                  @[simp]
                                                                  theorem AddMonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] {f : F} {y : N} :
                                                                  y AddMonoidHom.mrange f x, f x = y
                                                                  @[simp]
                                                                  theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] {f : F} {y : N} :
                                                                  y MonoidHom.mrange f x, f x = y
                                                                  theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :
                                                                  theorem MonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) :
                                                                  @[simp]
                                                                  theorem AddMonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) (hf : Function.Surjective f) :

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

                                                                  @[simp]
                                                                  theorem MonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (hf : Function.Surjective f) :

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

                                                                  theorem MonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (s : Set N) :
                                                                  theorem AddMonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) (s : Set M) :

                                                                  The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set.

                                                                  theorem MonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (s : Set M) :

                                                                  The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.

                                                                  def AddMonoidHom.restrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) :
                                                                  { x // x s } →+ N

                                                                  Restriction of an AddMonoid hom to an AddSubmonoid of the domain.

                                                                  Instances For
                                                                    def MonoidHom.restrict {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) :
                                                                    { x // x s } →* N

                                                                    Restriction of a monoid hom to a submonoid of the domain.

                                                                    Instances For
                                                                      @[simp]
                                                                      theorem AddMonoidHom.restrict_apply {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : { x // x s }) :
                                                                      ↑(AddMonoidHom.restrict f s) x = f x
                                                                      @[simp]
                                                                      theorem MonoidHom.restrict_apply {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) (x : { x // x s }) :
                                                                      ↑(MonoidHom.restrict f s) x = f x
                                                                      @[simp]
                                                                      def AddMonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_6} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) :
                                                                      M →+ { x // x s }

                                                                      Restriction of an AddMonoid hom to an AddSubmonoid of the codomain.

                                                                      Instances For
                                                                        theorem AddMonoidHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) :
                                                                        (fun n => { val := f n, property := h n }) 0 = 0
                                                                        theorem AddMonoidHom.codRestrict.proof_2 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) (x : M) (y : M) :
                                                                        ZeroHom.toFun { toFun := fun n => { val := f n, property := h n }, map_zero' := (_ : (fun n => { val := f n, property := h n }) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun n => { val := f n, property := h n }, map_zero' := (_ : (fun n => { val := f n, property := h n }) 0 = 0) } x + ZeroHom.toFun { toFun := fun n => { val := f n, property := h n }, map_zero' := (_ : (fun n => { val := f n, property := h n }) 0 = 0) } y
                                                                        @[simp]
                                                                        theorem AddMonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_6} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
                                                                        ↑(AddMonoidHom.codRestrict f s h) n = { val := f n, property := h n }
                                                                        @[simp]
                                                                        theorem MonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
                                                                        ↑(MonoidHom.codRestrict f s h) n = { val := f n, property := h n }
                                                                        def MonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) :
                                                                        M →* { x // x s }

                                                                        Restriction of a monoid hom to a submonoid of the codomain.

                                                                        Instances For
                                                                          theorem AddMonoidHom.mrangeRestrict.proof_1 {M : Type u_1} [AddZeroClass M] {N : Type u_2} [AddZeroClass N] (f : M →+ N) (x : M) :
                                                                          y, f y = f x
                                                                          def AddMonoidHom.mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} [AddZeroClass N] (f : M →+ N) :

                                                                          Restriction of an AddMonoid hom to its range interpreted as a submonoid.

                                                                          Instances For
                                                                            def MonoidHom.mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_6} [MulOneClass N] (f : M →* N) :
                                                                            M →* { x // x MonoidHom.mrange f }

                                                                            Restriction of a monoid hom to its range interpreted as a submonoid.

                                                                            Instances For
                                                                              @[simp]
                                                                              theorem AddMonoidHom.coe_mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} [AddZeroClass N] (f : M →+ N) (x : M) :
                                                                              ↑(↑(AddMonoidHom.mrangeRestrict f) x) = f x
                                                                              @[simp]
                                                                              theorem MonoidHom.coe_mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_6} [MulOneClass N] (f : M →* N) (x : M) :
                                                                              ↑(↑(MonoidHom.mrangeRestrict f) x) = f x
                                                                              abbrev AddMonoidHom.mrangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (motive : { x // x AddMonoidHom.mrange f }Prop) :
                                                                              (x : { x // x AddMonoidHom.mrange f }) → ((x : M) → motive { val := f x, property := (_ : y, f y = f x) }) → motive x
                                                                              Instances For
                                                                                def AddMonoidHom.mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) :

                                                                                The additive kernel of an AddMonoid hom is the AddSubmonoid of elements such that f x = 0

                                                                                Instances For
                                                                                  def MonoidHom.mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :

                                                                                  The multiplicative kernel of a monoid hom is the submonoid of elements x : G such that f x = 1

                                                                                  Instances For
                                                                                    theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) {x : M} :
                                                                                    x AddMonoidHom.mker f f x = 0
                                                                                    theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) {x : M} :
                                                                                    x MonoidHom.mker f f x = 1
                                                                                    theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) :
                                                                                    ↑(AddMonoidHom.mker f) = f ⁻¹' {0}
                                                                                    theorem MonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :
                                                                                    ↑(MonoidHom.mker f) = f ⁻¹' {1}
                                                                                    instance AddMonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] [DecidableEq N] (f : F) :
                                                                                    instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] [DecidableEq N] (f : F) :
                                                                                    theorem MonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) :
                                                                                    @[simp]
                                                                                    theorem AddMonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) :
                                                                                    @[simp]
                                                                                    theorem MonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) :
                                                                                    @[simp]
                                                                                    @[simp]
                                                                                    theorem MonoidHom.mker_one {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                                                                    theorem AddMonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [