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_symm_apply_coe {M : Type u_1} [MulOneClass M] (S : AddSubmonoid (Additive M)) :
((RelIso.symm Submonoid.toAddSubmonoid) S) = Additive.ofMul ⁻¹' S
@[simp]
theorem Submonoid.toAddSubmonoid_apply_coe {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
(Submonoid.toAddSubmonoid S) = Additive.toMul ⁻¹' S

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

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

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

    Equations
    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.

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

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

        Equations
        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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

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

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

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

            Equations
            Instances For
              @[simp]
              theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M} :
              @[simp]
              theorem Submonoid.mem_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M} :
              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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

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

              Equations
              • AddSubmonoid.map f S = { toAddSubsemigroup := { carrier := f '' S, add_mem' := }, zero_mem' := }
              Instances For
                theorem AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :
                ∃ a ∈ S, f a = 0
                def Submonoid.map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

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

                Equations
                • Submonoid.map f S = { toSubsemigroup := { carrier := f '' S, mul_mem' := }, one_mem' := }
                Instances For
                  @[simp]
                  theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N} :
                  y AddSubmonoid.map f S ∃ 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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N} :
                  y Submonoid.map f S ∃ 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} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M} (hx : x S) :
                  theorem AddSubmonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : S) :
                  theorem Submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (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} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : AddSubmonoid M} {x : M} :
                  @[simp]
                  theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N} :
                  theorem AddSubmonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :
                  theorem Submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :
                  @[simp]
                  theorem AddSubmonoid.map_comap_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :
                  @[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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :
                  @[simp]
                  @[simp]
                  theorem Submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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 )motive x_1
                  Equations
                  • =
                  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} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : AddSubmonoid M) (x : M) :
                    def AddSubmonoid.gciMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) :

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

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

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

                      Equations
                      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} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : Submonoid M) :
                        theorem Submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :
                        theorem Submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :
                        theorem AddSubmonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : AddSubmonoid M) (T : AddSubmonoid M) :
                        theorem Submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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 AddSubmonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) (S : AddSubmonoid M) (T : AddSubmonoid M) :
                        theorem Submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) {S : Submonoid M} {T : Submonoid M} :
                        theorem AddSubmonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective f) :
                        theorem Submonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective f) :
                        abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} {F : Type u_3} [FunLike F M N] {f : F} (x : N) (motive : (∃ (a : M), f a = x)Prop) :
                        ∀ (x_1 : ∃ (a : M), f a = x), (∀ (y : M) (hy : f y = x), motive )motive x_1
                        Equations
                        • =
                        Instances For
                          def AddSubmonoid.giMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :

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

                          Equations
                          Instances For
                            theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [FunLike F M N] [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} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :

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

                            Equations
                            Instances For
                              theorem AddSubmonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : AddSubmonoid N) :
                              theorem Submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) (S : Submonoid N) :
                              theorem Submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :
                              theorem Submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective f) :
                              theorem Submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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 S'

                              An AddSubmonoid of an AddMonoid inherits a zero.

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

                              A submonoid of a monoid inherits a 1.

                              Equations
                              @[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 : 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 : 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 := }
                              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 := }
                              instance AddSubmonoidClass.nSMul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              SMul S

                              An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

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

                              A submonoid of a monoid inherits a power operator.

                              Equations
                              @[simp]
                              theorem AddSubmonoidClass.coe_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] {S : A} (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 : 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 := }
                              @[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 := }
                              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 : S), (x + x_1) = (x + x_1)
                              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) :

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

                              Equations
                              theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun (a : S) => a
                              instance SubmonoidClass.toMulOneClass {M : Type u_5} [MulOneClass M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) :

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

                              Equations
                              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 : S), (x + x_1) = (x + x_1)
                              instance AddSubmonoidClass.toAddMonoid {M : Type u_5} [AddMonoid M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) :

                              An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

                              Equations
                              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 : S) (x_1 : ), (x_1 x) = (x_1 x)
                              theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun (a : S) => a
                              instance SubmonoidClass.toMonoid {M : Type u_5} [Monoid M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) :
                              Monoid S

                              A submonoid of a monoid inherits a monoid structure.

                              Equations
                              theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                              Function.Injective fun (a : S) => a
                              theorem AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                              ∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
                              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 : S), (x + x_1) = (x + x_1)
                              instance SubmonoidClass.toCommMonoid {M : Type u_6} [CommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) :

                              A submonoid of a CommMonoid is a CommMonoid.

                              Equations
                              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
                              theorem AddSubmonoidClass.subtype.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] (S' : A) :
                              ∀ (x x_1 : S'), x + x_1 = x + x_1
                              def AddSubmonoidClass.subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :
                              S' →+ M

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

                              Equations
                              Instances For
                                def SubmonoidClass.subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [SetLike A M] [hA : SubmonoidClass A M] (S' : A) :
                                S' →* M

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

                                Equations
                                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
                                  theorem AddSubmonoid.add.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (a : S) (b : S) :
                                  a + b S
                                  instance AddSubmonoid.add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  Add S

                                  An AddSubmonoid of an AddMonoid inherits an addition.

                                  Equations
                                  • AddSubmonoid.add S = { add := fun (a b : S) => { val := a + b, property := } }
                                  instance Submonoid.mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  Mul S

                                  A submonoid of a monoid inherits a multiplication.

                                  Equations
                                  • Submonoid.mul S = { mul := fun (a b : S) => { val := a * b, property := } }
                                  instance AddSubmonoid.zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  Zero S

                                  An AddSubmonoid of an AddMonoid inherits a zero.

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

                                  A submonoid of a monoid inherits a 1.

                                  Equations
                                  @[simp]
                                  theorem AddSubmonoid.coe_add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : S) (y : S) :
                                  (x + y) = x + y
                                  @[simp]
                                  theorem Submonoid.coe_mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : S) (y : 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_eq_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) {a : M} {ha : a S} :
                                  { val := a, property := ha } = 0 a = 0
                                  @[simp]
                                  theorem Submonoid.mk_eq_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) {a : M} {ha : a S} :
                                  { val := a, property := ha } = 1 a = 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 := }
                                  @[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 := }
                                  theorem AddSubmonoid.add_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : S) (y : S) :
                                  x + y = { val := x + y, property := }
                                  theorem Submonoid.mul_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : S) (y : S) :
                                  x * y = { val := x * y, property := }
                                  theorem AddSubmonoid.zero_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  0 = { val := 0, property := }
                                  theorem Submonoid.one_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  1 = { val := 1, property := }
                                  theorem AddSubmonoid.toAddZeroClass.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  Function.Injective fun (a : S) => a
                                  theorem AddSubmonoid.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : S), (x + x_1) = (x + x_1)

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

                                  Equations
                                  instance Submonoid.toMulOneClass {M : Type u_5} [MulOneClass M] (S : Submonoid M) :

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

                                  Equations
                                  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 : S) (x_1 : ), (x_1 x) = (x_1 x)
                                  theorem AddSubmonoid.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  0 = 0
                                  theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  ∀ (x x_1 : S), (x + x_1) = (x + x_1)
                                  theorem AddSubmonoid.toAddMonoid.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                                  Function.Injective fun (a : S) => a
                                  instance AddSubmonoid.toAddMonoid {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) :

                                  An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

                                  Equations
                                  instance Submonoid.toMonoid {M : Type u_5} [Monoid M] (S : Submonoid M) :
                                  Monoid S

                                  A submonoid of a monoid inherits a monoid structure.

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

                                  A submonoid of a CommMonoid is a CommMonoid.

                                  Equations
                                  def AddSubmonoid.subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  S →+ M

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

                                  Equations
                                  Instances For
                                    theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                    0 = 0
                                    theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                    ∀ (x x_1 : S), x + x_1 = x + x_1
                                    def Submonoid.subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                    S →* M

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

                                    Equations
                                    • Submonoid.subtype S = { toOneHom := { toFun := Subtype.val, map_one' := }, map_mul' := }
                                    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

                                      The top additive submonoid is isomorphic to the additive monoid.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [AddZeroClass M] (x : ) :
                                        { val := x, property := } = x
                                        theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] :
                                        ∀ (x : M), (fun (x : ) => x) ((fun (x : M) => { val := x, property := }) x) = (fun (x : ) => x) ((fun (x : M) => { val := x, property := }) x)
                                        theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [AddZeroClass M] :
                                        ∀ (x x_1 : ), { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }.toFun (x + x_1)
                                        @[simp]
                                        theorem AddSubmonoid.topEquiv_apply {M : Type u_1} [AddZeroClass M] (x : ) :
                                        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 Submonoid.topEquiv_apply {M : Type u_1} [MulOneClass M] (x : ) :
                                        Submonoid.topEquiv x = x
                                        @[simp]
                                        theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_1} [AddZeroClass M] (x : M) :
                                        ((AddEquiv.symm AddSubmonoid.topEquiv) x) = x
                                        def Submonoid.topEquiv {M : Type u_1} [MulOneClass M] :
                                        ≃* M

                                        The top submonoid is isomorphic to the monoid.

                                        Equations
                                        • Submonoid.topEquiv = { toEquiv := { toFun := fun (x : ) => x, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }, map_mul' := }
                                        Instances For
                                          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) :
                                          ∀ (x x_1 : S), (Equiv.Set.image (f) (S) hf).toFun (x + x_1) = (Equiv.Set.image (f) (S) hf).toFun x + (Equiv.Set.image (f) (S) hf).toFun x_1
                                          noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective f) :
                                          S ≃+ (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.

                                          Equations
                                          Instances For
                                            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) :
                                            S ≃* (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.

                                            Equations
                                            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 : 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 : S) :
                                              ((Submonoid.equivMapOfInjective S f hf) x) = f x
                                              @[simp]
                                              theorem AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                              0.1 s 0.2 t
                                              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).1 s (a + b).2 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.

                                              Equations
                                              • AddSubmonoid.prod s t = { toAddSubsemigroup := { carrier := s ×ˢ t, add_mem' := }, zero_mem' := }
                                              Instances For
                                                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.

                                                Equations
                                                • Submonoid.prod s t = { toSubsemigroup := { carrier := s ×ˢ t, mul_mem' := }, one_mem' := }
                                                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.1 s p.2 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.1 s p.2 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₂
                                                  def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                  (AddSubmonoid.prod s t) ≃+ s × t

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

                                                  Equations
                                                  Instances For
                                                    theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                    ∀ (x x_1 : (AddSubmonoid.prod s t)), (Equiv.Set.prod s t).toFun (x + x_1) = (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) :
                                                    (Submonoid.prod s t) ≃* s × t

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

                                                    Equations
                                                    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.1 s) (hp1 : p.2 ), motive )motive x
                                                      Equations
                                                      • =
                                                      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 )motive x
                                                        Equations
                                                        • =
                                                        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 )motive x
                                                          Equations
                                                          • =
                                                          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.1 ) (hps : p.2 s), motive )motive x
                                                            Equations
                                                            • =
                                                            Instances For
                                                              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} {F : Type u_3} [FunLike 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} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

                                                              The range of an AddMonoidHom is an AddSubmonoid.

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

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

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {y : N} :
                                                                  y AddMonoidHom.mrange f ∃ (x : M), f x = y
                                                                  @[simp]
                                                                  theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {y : N} :
                                                                  y MonoidHom.mrange f ∃ (x : M), f x = y
                                                                  theorem AddMonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :
                                                                  theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [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) :
                                                                  theorem MonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :
                                                                  @[simp]
                                                                  theorem AddMonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [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) :
                                                                  s →+ N

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

                                                                  Equations
                                                                  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) :
                                                                    s →* N

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

                                                                    Equations
                                                                    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 : 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 : s) :
                                                                      (MonoidHom.restrict f s) x = f x
                                                                      @[simp]
                                                                      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) :
                                                                      { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun x + { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }.toFun y
                                                                      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 →+ s

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

                                                                      Equations
                                                                      • AddMonoidHom.codRestrict f s h = { toZeroHom := { toFun := fun (n : M) => { val := f n, property := }, map_zero' := }, map_add' := }
                                                                      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 : M) => { val := f n, property := }) 0 = 0
                                                                        @[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 := }
                                                                        @[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 := }
                                                                        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 →* s

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

                                                                        Equations
                                                                        • MonoidHom.codRestrict f s h = { toOneHom := { toFun := fun (n : M) => { val := f n, property := }, map_one' := }, map_mul' := }
                                                                        Instances For
                                                                          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.

                                                                          Equations
                                                                          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 : M), f y = f x
                                                                            def MonoidHom.mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_6} [MulOneClass N] (f : M →* N) :

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

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

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

                                                                                Equations
                                                                                Instances For
                                                                                  def MonoidHom.mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [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

                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) {x : M} :
                                                                                    theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) {x : M} :
                                                                                    theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [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} [FunLike F M N] [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} [FunLike F M N] [mc : AddMonoidHomClass F M N] [DecidableEq N] (f : F) :
                                                                                    Equations
                                                                                    instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] [DecidableEq N] (f : F) :
                                                                                    DecidablePred fun (x : M) => x MonoidHom.mker f
                                                                                    Equations
                                                                                    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} [FunLike F M N] [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} [FunLike F M N] [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 MonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') (S : Submonoid N) (S' : Submonoid N') :
                                                                                    theorem MonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') :
                                                                                    @[simp]
                                                                                    @[simp]
                                                                                    theorem AddMonoidHom.addSubmonoidComap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : (AddSubmonoid.comap f N')) (y : (AddSubmonoid.comap f N')) :
                                                                                    { toFun := fun (x : (AddSubmonoid.comap f N')) => { val := f x, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (x : (AddSubmonoid.comap f N')) => { val := f x, property := }, map_zero' := }.toFun x + { toFun := fun (x : (AddSubmonoid.comap f N')) => { val := f x, property := }, map_zero' := }.toFun y
                                                                                    theorem AddMonoidHom.addSubmonoidComap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) :
                                                                                    (fun (x : (AddSubmonoid.comap f N')) => { val := f x, property := }) 0 = 0
                                                                                    def AddMonoidHom.addSubmonoidComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) :
                                                                                    (AddSubmonoid.comap f N') →+ N'

                                                                                    the AddMonoidHom from the preimage of an additive submonoid to itself.

                                                                                    Equations
                                                                                    Instances For
                                                                                      theorem AddMonoidHom.addSubmonoidComap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : (AddSubmonoid.comap f N')) :
                                                                                      @[simp]
                                                                                      theorem AddMonoidHom.addSubmonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : (AddSubmonoid.comap f N')) :
                                                                                      ((AddMonoidHom.addSubmonoidComap f N') x) = f x
                                                                                      @[simp]
                                                                                      theorem MonoidHom.submonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (x : (Submonoid.comap f N')) :
                                                                                      ((MonoidHom.submonoidComap f N') x) = f x
                                                                                      def MonoidHom.submonoidComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) :
                                                                                      (Submonoid.comap f N') →* N'

                                                                                      The MonoidHom from the preimage of a submonoid to itself.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem AddMonoidHom.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : M') (y : M') :
                                                                                        { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun x + { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }.toFun y
                                                                                        theorem AddMonoidHom.addSubmonoidMap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :
                                                                                        (fun (x : M') => { val := f x, property := }) 0 = 0
                                                                                        theorem AddMonoidHom.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : M') :
                                                                                        ∃ a ∈ M', f a = f x
                                                                                        def AddMonoidHom.addSubmonoidMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :
                                                                                        M' →+ (AddSubmonoid.map f M')

                                                                                        the AddMonoidHom from an additive submonoid to its image. See AddEquiv.AddSubmonoidMap for a variant for AddEquivs.

                                                                                        Equations
                                                                                        • AddMonoidHom.addSubmonoidMap f M' = { toZeroHom := { toFun := fun (x : M') => { val := f x, property := }, map_zero' := }, map_add' := }
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem MonoidHom.submonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) (x : M') :
                                                                                          ((MonoidHom.submonoidMap f M') x) = f x
                                                                                          @[simp]
                                                                                          theorem AddMonoidHom.addSubmonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : M') :
                                                                                          ((AddMonoidHom.addSubmonoidMap f M') x) = f x
                                                                                          def MonoidHom.submonoidMap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) :
                                                                                          M' →* (Submonoid.map f M')

                                                                                          The MonoidHom from a submonoid to its image. See MulEquiv.SubmonoidMap for a variant for MulEquivs.

                                                                                          Equations
                                                                                          • MonoidHom.submonoidMap f M' = { toOneHom := { toFun := fun (x : M') => { val := f x, property := }, map_one' := }, map_mul' := }
                                                                                          Instances For
                                                                                            theorem Submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :
                                                                                            theorem AddSubmonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} :