Documentation

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

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

    Equations
    • AddSubmonoid.toSubmonoid' = Submonoid.toAddSubmonoid.symm
    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
        @[reducible, inline]

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

        Equations
        • Submonoid.toAddSubmonoid' = AddSubmonoid.toSubmonoid.symm
        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_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :
          f 0 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
            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 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 AddSubmonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N) :
              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_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) :
              aS, f a = 0
              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
              Instances For
                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 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 = { 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 xS, 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 xS, 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.map_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 M) (T : AddSubmonoid M) (f : F) (hf : Function.Injective f) :
                  theorem Submonoid.map_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 M) (T : Submonoid M) (f : F) (hf : Function.Injective f) :
                  theorem AddSubmonoid.map_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} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ιAddSubmonoid M) :
                  AddSubmonoid.map f (iInf s) = ⨅ (i : ι), AddSubmonoid.map f (s i)
                  theorem Submonoid.map_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} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ιSubmonoid M) :
                  Submonoid.map f (iInf 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) :
                  @[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_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [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) :
                      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_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [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 = 0,
                          theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) :
                          1 = 1,
                          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 x, hx = n x,
                          @[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 : ) :
                          x, hx ^ n = x ^ n,
                          @[instance 75]
                          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
                          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
                          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)
                          @[instance 75]
                          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)
                          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_3 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) :
                          0 = 0
                          @[instance 75]
                          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_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                          Function.Injective fun (a : S) => a
                          @[instance 75]
                          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_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_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)
                          @[instance 75]
                          instance AddSubmonoidClass.toAddCommMonoid {M : Type u_6} [AddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) :

                          An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

                          Equations
                          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)
                          theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
                          Function.Injective fun (a : S) => a
                          @[instance 75]
                          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
                              instance AddSubmonoid.add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                              Add S

                              An AddSubmonoid of an AddMonoid inherits an addition.

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

                              A submonoid of a monoid inherits a multiplication.

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

                              An AddSubmonoid of an AddMonoid inherits a zero.

                              Equations
                              • S.zero = { zero := 0, }
                              instance Submonoid.one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                              One S

                              A submonoid of a monoid inherits a 1.

                              Equations
                              • S.one = { one := 1, }
                              @[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} :
                              a, ha = 0 a = 0
                              @[simp]
                              theorem Submonoid.mk_eq_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) {a : M} {ha : a S} :
                              a, 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) :
                              x, hx + y, hy = x + y,
                              @[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) :
                              x, hx * y, hy = x * y,
                              theorem AddSubmonoid.add_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : S) (y : S) :
                              x + y = x + y,
                              theorem Submonoid.mul_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : S) (y : S) :
                              x * y = x * y,
                              theorem AddSubmonoid.zero_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                              0 = 0,
                              theorem Submonoid.one_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                              1 = 1,
                              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
                              theorem AddSubmonoid.toAddZeroClass.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                              Function.Injective fun (a : S) => a
                              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_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
                              theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                              ∀ (x x_1 : S), (x + x_1) = (x + x_1)
                              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_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                              ∀ (x x_1 : S), (x + x_1) = (x + x_1)
                              theorem AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :
                              ∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)

                              An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

                              Equations
                              instance Submonoid.toCommMonoid {M : Type u_5} [CommMonoid M] (S : Submonoid M) :

                              A submonoid of a CommMonoid is a CommMonoid.

                              Equations
                              theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                              ∀ (x x_1 : 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) :
                              S →+ M

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

                              Equations
                              • S.subtype = { toFun := Subtype.val, map_zero' := , map_add' := }
                              Instances For
                                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
                                • S.subtype = { toFun := Subtype.val, map_one' := , map_mul' := }
                                Instances For
                                  @[simp]
                                  theorem AddSubmonoid.coe_subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                  S.subtype = Subtype.val
                                  @[simp]
                                  theorem Submonoid.coe_subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                  S.subtype = Subtype.val
                                  theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] :
                                  ∀ (x : M), (fun (x : ) => x) ((fun (x : M) => x, ) x) = (fun (x : ) => x) ((fun (x : M) => x, ) x)

                                  The top additive submonoid is isomorphic to the additive monoid.

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

                                    The top submonoid is isomorphic to the monoid.

                                    Equations
                                    • Submonoid.topEquiv = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_mul' := }
                                    Instances For
                                      @[simp]
                                      theorem AddSubmonoid.topEquiv_toAddMonoidHom {M : Type u_1} [AddZeroClass M] :
                                      AddSubmonoid.topEquiv = .subtype
                                      @[simp]
                                      theorem Submonoid.topEquiv_toMonoidHom {M : Type u_1} [MulOneClass M] :
                                      Submonoid.topEquiv = .subtype
                                      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
                                      • S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := }
                                      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 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
                                        • S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := }
                                        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) :
                                          ((S.equivMapOfInjective 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) :
                                          ((S.equivMapOfInjective 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
                                          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
                                          • s.prod t = { carrier := s ×ˢ t, add_mem' := , zero_mem' := }
                                          Instances For
                                            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 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
                                            • s.prod t = { 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) :
                                              (s.prod 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) :
                                              (s.prod 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 s.prod 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 s.prod 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₂) :
                                              s₁.prod t₁ s₂.prod 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₂) :
                                              s₁.prod t₁ s₂.prod t₂
                                              theorem Submonoid.prod_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) :
                                              theorem Submonoid.top_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid N) :
                                              @[simp]
                                              theorem AddSubmonoid.top_prod_top {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                              .prod =
                                              @[simp]
                                              theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                              .prod =
                                              theorem AddSubmonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :
                                              .prod =
                                              theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                              .prod =
                                              def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                              (s.prod 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 : (s.prod 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) :
                                                (s.prod t) ≃* s × t

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

                                                Equations
                                                Instances For
                                                  theorem Submonoid.map_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) :
                                                  theorem Submonoid.map_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid N) :
                                                  @[simp]
                                                  theorem AddSubmonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :
                                                  s.prod .prod t = s.prod t
                                                  @[simp]
                                                  theorem Submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) (t : Submonoid N) :
                                                  s.prod .prod t = s.prod t
                                                  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} :
                                                  x AddSubmonoid.map f.toAddMonoidHom K f.symm x K
                                                  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} :
                                                  x Submonoid.map f.toMonoidHom K f.symm x K
                                                  theorem AddSubmonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) (K : AddSubmonoid M) :
                                                  AddSubmonoid.map f.toAddMonoidHom K = AddSubmonoid.comap f.symm.toAddMonoidHom K
                                                  theorem Submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M ≃* N) (K : Submonoid M) :
                                                  Submonoid.map f.toMonoidHom K = Submonoid.comap f.symm.toMonoidHom K
                                                  theorem Submonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : N ≃* M) (K : Submonoid M) :
                                                  @[simp]
                                                  theorem AddSubmonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) :
                                                  @[simp]
                                                  theorem Submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M ≃* N) :
                                                  theorem Submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
                                                  theorem Submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
                                                  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
                                                    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 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 AddMonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) :
                                                      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.

                                                      @[simp]
                                                      theorem AddMonoidHom.mclosure_range {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.mclosure_range {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) :
                                                      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) :
                                                          (f.restrict 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) :
                                                          (f.restrict s) x = f x
                                                          @[simp]
                                                          theorem AddMonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) :
                                                          @[simp]
                                                          theorem MonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) :
                                                          MonoidHom.mrange (f.restrict S) = Submonoid.map f S
                                                          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) => f n, ) 0 = 0
                                                          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
                                                          • f.codRestrict s h = { toFun := fun (n : M) => f n, , map_zero' := , map_add' := }
                                                          Instances For
                                                            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) => f n, , map_zero' := }.toFun (x + y) = { toFun := fun (n : M) => f n, , map_zero' := }.toFun x + { toFun := fun (n : M) => f n, , map_zero' := }.toFun 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) :
                                                            (f.codRestrict s h) n = f 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) :
                                                            (f.codRestrict s h) n = f 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 →* s

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

                                                            Equations
                                                            • f.codRestrict s h = { toFun := fun (n : M) => f n, , map_one' := , map_mul' := }
                                                            Instances For
                                                              @[simp]
                                                              theorem AddMonoidHom.injective_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) :
                                                              Function.Injective (f.codRestrict s h) Function.Injective f
                                                              @[simp]
                                                              theorem MonoidHom.injective_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) :
                                                              Function.Injective (f.codRestrict s h) Function.Injective f
                                                              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 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
                                                                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) :
                                                                  (f.mrangeRestrict 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) :
                                                                  (f.mrangeRestrict x) = f x
                                                                  theorem AddMonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                                  Function.Surjective f.mrangeRestrict
                                                                  theorem MonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                                  Function.Surjective f.mrangeRestrict
                                                                  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
                                                                      @[simp]
                                                                      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} :
                                                                      @[simp]
                                                                      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 AddMonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) :
                                                                      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]
                                                                      theorem AddMonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) :
                                                                      @[simp]
                                                                      theorem MonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) :
                                                                      MonoidHom.mker (f.restrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)
                                                                      theorem AddMonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                                      theorem MonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                                      MonoidHom.mker f.mrangeRestrict = MonoidHom.mker 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'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') (S : AddSubmonoid N) (S' : AddSubmonoid N') :
                                                                      AddSubmonoid.comap (f.prodMap g) (S.prod S') = (AddSubmonoid.comap f S).prod (AddSubmonoid.comap g S')
                                                                      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') :
                                                                      Submonoid.comap (f.prodMap g) (S.prod S') = (Submonoid.comap f S).prod (Submonoid.comap g S')
                                                                      theorem AddMonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ 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') :
                                                                      MonoidHom.mker (f.prodMap g) = (MonoidHom.mker f).prod (MonoidHom.mker g)
                                                                      @[simp]
                                                                      @[simp]
                                                                      @[simp]
                                                                      theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                                                      @[simp]
                                                                      theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :
                                                                      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')) => f x, ) 0 = 0
                                                                      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')) => f x, , map_zero' := }.toFun (x + y) = { toFun := fun (x : (AddSubmonoid.comap f N')) => f x, , map_zero' := }.toFun x + { toFun := fun (x : (AddSubmonoid.comap f N')) => f x, , map_zero' := }.toFun y
                                                                      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
                                                                      • f.addSubmonoidComap N' = { toFun := fun (x : (AddSubmonoid.comap f N')) => f x, , map_zero' := , map_add' := }
                                                                      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 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')) :
                                                                        ((f.submonoidComap N') x) = f x
                                                                        @[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')) :
                                                                        ((f.addSubmonoidComap 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
                                                                        • f.submonoidComap N' = { toFun := fun (x : (Submonoid.comap f N')) => f x, , map_one' := , map_mul' := }
                                                                        Instances For
                                                                          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') :
                                                                          aM', f a = f x
                                                                          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') => f x, ) 0 = 0
                                                                          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
                                                                          • f.addSubmonoidMap M' = { toFun := fun (x : M') => f x, , map_zero' := , map_add' := }
                                                                          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') => f x, , map_zero' := }.toFun (x + y) = { toFun := fun (x : M') => f x, , map_zero' := }.toFun x + { toFun := fun (x : M') => f x, , map_zero' := }.toFun y
                                                                            @[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') :
                                                                            ((f.addSubmonoidMap M') x) = f x
                                                                            @[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') :
                                                                            ((f.submonoidMap 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
                                                                            • f.submonoidMap M' = { toFun := fun (x : M') => f x, , map_one' := , map_mul' := }
                                                                            Instances For
                                                                              theorem AddMonoidHom.addSubmonoidMap_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :
                                                                              Function.Surjective (f.addSubmonoidMap M')
                                                                              theorem MonoidHom.submonoidMap_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) :
                                                                              Function.Surjective (f.submonoidMap M')
                                                                              theorem AddSubmonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} :
                                                                              s.prod t = s = t =
                                                                              theorem Submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :
                                                                              s.prod t = s = t =
                                                                              theorem AddSubmonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} :
                                                                              s.prod t = s = t =
                                                                              theorem Submonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :
                                                                              s.prod t = s = t =
                                                                              def AddSubmonoid.inclusion {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S T) :
                                                                              S →+ T

                                                                              The AddMonoid hom associated to an inclusion of submonoids.

                                                                              Equations
                                                                              Instances For
                                                                                theorem AddSubmonoid.inclusion.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S T) (x : S) :
                                                                                S.subtype x T
                                                                                def Submonoid.inclusion {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S T) :
                                                                                S →* T

                                                                                The monoid hom associated to an inclusion of submonoids.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  @[simp]
                                                                                  theorem Submonoid.range_subtype {M : Type u_1} [MulOneClass M] (s : Submonoid M) :
                                                                                  MonoidHom.mrange s.subtype = s
                                                                                  theorem AddSubmonoid.eq_top_iff' {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                                                                  S = ∀ (x : M), x S
                                                                                  theorem Submonoid.eq_top_iff' {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                                                                  S = ∀ (x : M), x S
                                                                                  theorem AddSubmonoid.eq_bot_iff_forall {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                                                                  S = xS, x = 0
                                                                                  theorem Submonoid.eq_bot_iff_forall {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                                                                  S = xS, x = 1
                                                                                  theorem Submonoid.nontrivial_iff_exists_ne_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                                                                  Nontrivial S xS, x 1

                                                                                  An additive submonoid is either the trivial additive submonoid or nontrivial.

                                                                                  A submonoid is either the trivial submonoid or nontrivial.

                                                                                  theorem AddSubmonoid.bot_or_exists_ne_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :
                                                                                  S = xS, x 0

                                                                                  An additive submonoid is either the trivial additive submonoid or contains a nonzero element.

                                                                                  theorem Submonoid.bot_or_exists_ne_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :
                                                                                  S = xS, x 1

                                                                                  A submonoid is either the trivial submonoid or contains a nonzero element.

                                                                                  theorem AddEquiv.addSubmonoidCongr.proof_2 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :
                                                                                  ∀ (x x_1 : S), (Equiv.setCongr ).toFun (x + x_1) = (Equiv.setCongr ).toFun (x + x_1)
                                                                                  theorem AddEquiv.addSubmonoidCongr.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :
                                                                                  S = T
                                                                                  def AddEquiv.addSubmonoidCongr {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :
                                                                                  S ≃+ T

                                                                                  Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def MulEquiv.submonoidCongr {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S = T) :
                                                                                    S ≃* T

                                                                                    Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.

                                                                                    Equations
                                                                                    Instances For
                                                                                      theorem AddEquiv.ofLeftInverse'.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : M) (y : M) :
                                                                                      (↑f.mrangeRestrict).toFun (x + y) = (↑f.mrangeRestrict).toFun x + (↑f.mrangeRestrict).toFun y
                                                                                      def AddEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : NM} (h : Function.LeftInverse g f) :

                                                                                      An additive monoid homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.mrange. This is a bidirectional version of AddMonoidHom.mrange_restrict.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem AddEquiv.ofLeftInverse'.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : NM} (h : Function.LeftInverse g f) (x : (AddMonoidHom.mrange f)) :
                                                                                        f.mrangeRestrict ((g (AddMonoidHom.mrange f).subtype) x) = x
                                                                                        @[simp]
                                                                                        theorem AddEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
                                                                                        (AddEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a
                                                                                        @[simp]
                                                                                        theorem AddEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : NM} (h : Function.LeftInverse g f) :
                                                                                        ∀ (a : (AddMonoidHom.mrange f)), (AddEquiv.ofLeftInverse' f h).symm a = g a
                                                                                        @[simp]
                                                                                        theorem MulEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
                                                                                        (MulEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a
                                                                                        @[simp]
                                                                                        theorem MulEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : NM} (h : Function.LeftInverse g f) :
                                                                                        ∀ (a : (MonoidHom.mrange f)), (MulEquiv.ofLeftInverse' f h).symm a = g a
                                                                                        def MulEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : NM} (h : Function.LeftInverse g f) :

                                                                                        A monoid homomorphism f : M →* N with a left-inverse g : N → M defines a multiplicative equivalence between M and f.mrange. This is a bidirectional version of MonoidHom.mrange_restrict.

                                                                                        Equations
                                                                                        Instances For
                                                                                          def AddEquiv.addSubmonoidMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :
                                                                                          S ≃+ (AddSubmonoid.map e S)

                                                                                          An AddEquiv φ between two additive monoids M and N induces an AddEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See AddMonoidHom.addSubmonoidMap for a variant for AddMonoidHoms.

                                                                                          Equations
                                                                                          • e.addSubmonoidMap S = { toEquiv := (↑e).image S, map_add' := }
                                                                                          Instances For
                                                                                            theorem AddEquiv.addSubmonoidMap.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :
                                                                                            ∀ (x x_1 : S), ((↑e).image S).toFun (x + x_1) = ((↑e).image S).toFun x + ((↑e).image S).toFun x_1
                                                                                            def MulEquiv.submonoidMap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) :
                                                                                            S ≃* (Submonoid.map e S)

                                                                                            A MulEquiv φ between two monoids M and N induces a MulEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See MonoidHom.submonoidMap for a variant for MonoidHoms.

                                                                                            Equations
                                                                                            • e.submonoidMap S = { toEquiv := (↑e).image S, map_mul' := }
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem AddEquiv.coe_addSubmonoidMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : S) :
                                                                                              ((e.addSubmonoidMap S) g) = e g
                                                                                              @[simp]
                                                                                              theorem MulEquiv.coe_submonoidMap_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : S) :
                                                                                              ((e.submonoidMap S) g) = e g
                                                                                              @[simp]
                                                                                              theorem AddEquiv.add_submonoid_map_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : (AddSubmonoid.map (↑e) S)) :
                                                                                              (e.addSubmonoidMap S).symm g = e.symm g,
                                                                                              @[simp]
                                                                                              theorem MulEquiv.submonoidMap_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : (Submonoid.map (↑e) S)) :
                                                                                              (e.submonoidMap S).symm g = e.symm g,
                                                                                              @[simp]
                                                                                              theorem AddSubmonoid.equivMapOfInjective_coe_addEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (e : M ≃+ N) :
                                                                                              S.equivMapOfInjective e = e.addSubmonoidMap S
                                                                                              @[simp]
                                                                                              theorem Submonoid.equivMapOfInjective_coe_mulEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (e : M ≃* N) :
                                                                                              S.equivMapOfInjective e = e.submonoidMap S

                                                                                              Actions by Submonoids #

                                                                                              These instances transfer the action by an element m : M of a monoid M written as m • a onto the action by an element s : S of a submonoid S : Submonoid M such that s • a = (s : M) • a.

                                                                                              These instances work particularly well in conjunction with Monoid.toMulAction, enabling s • m as an alias for ↑s * m.

                                                                                              instance AddSubmonoid.vadd {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') :
                                                                                              VAdd (↥S) α
                                                                                              Equations
                                                                                              instance Submonoid.smul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] (S : Submonoid M') :
                                                                                              SMul (↥S) α
                                                                                              Equations
                                                                                              instance AddSubmonoid.vaddCommClass_left {M' : Type u_5} {α : Type u_6} {β : Type u_7} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') :
                                                                                              VAddCommClass (↥S) α β
                                                                                              Equations
                                                                                              • =
                                                                                              instance Submonoid.smulCommClass_left {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') :
                                                                                              SMulCommClass (↥S) α β
                                                                                              Equations
                                                                                              • =
                                                                                              instance AddSubmonoid.vaddCommClass_right {M' : Type u_5} {α : Type u_6} {β : Type u_7} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') :
                                                                                              VAddCommClass α (↥S) β
                                                                                              Equations
                                                                                              • =
                                                                                              instance Submonoid.smulCommClass_right {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') :
                                                                                              SMulCommClass α (↥S) β
                                                                                              Equations
                                                                                              • =
                                                                                              instance Submonoid.isScalarTower {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') :
                                                                                              IsScalarTower (↥S) α β

                                                                                              Note that this provides IsScalarTower S M' M' which is needed by SMulMulAssoc.

                                                                                              Equations
                                                                                              • =
                                                                                              theorem AddSubmonoid.vadd_def {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : S) (a : α) :
                                                                                              g +ᵥ a = g +ᵥ a
                                                                                              theorem Submonoid.smul_def {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : S) (a : α) :
                                                                                              g a = g a
                                                                                              @[simp]
                                                                                              theorem AddSubmonoid.mk_vadd {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : M') (hg : g S) (a : α) :
                                                                                              g, hg +ᵥ a = g +ᵥ a
                                                                                              @[simp]
                                                                                              theorem Submonoid.mk_smul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : M') (hg : g S) (a : α) :
                                                                                              g, hg a = g a
                                                                                              instance Submonoid.faithfulSMul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} [FaithfulSMul M' α] :
                                                                                              FaithfulSMul (↥S) α
                                                                                              Equations
                                                                                              • =
                                                                                              instance AddSubmonoid.addAction {M' : Type u_5} {α : Type u_6} [AddMonoid M'] [AddAction M' α] (S : AddSubmonoid M') :
                                                                                              AddAction (↥S) α

                                                                                              The additive action by an AddSubmonoid is the action by the underlying AddMonoid.

                                                                                              Equations
                                                                                              instance Submonoid.mulAction {M' : Type u_5} {α : Type u_6} [Monoid M'] [MulAction M' α] (S : Submonoid M') :
                                                                                              MulAction (↥S) α

                                                                                              The action by a submonoid is the action by the underlying monoid.

                                                                                              Equations
                                                                                              theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (x : AddUnits M) (y : AddUnits M) :
                                                                                              { toFun := fun (x : AddUnits M) => x, , invFun := fun (x : (IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit , left_inv := , right_inv := }.toFun (x + y) = { toFun := fun (x : AddUnits M) => x, , invFun := fun (x : (IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit , left_inv := , right_inv := }.toFun x + { toFun := fun (x : AddUnits M) => x, , invFun := fun (x : (IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit , left_inv := , right_inv := }.toFun y
                                                                                              theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.proof_3 {M : Type u_1} [AddMonoid M] (x : (IsAddUnit.addSubmonoid M)) :
                                                                                              (fun (x : AddUnits M) => x, ) ((fun (x : (IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ) x) = x

                                                                                              The additive equivalence between the type of additive units of M and the additive submonoid whose elements are the additive units of M.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_1} [Monoid M] (x : (IsUnit.submonoid M)) :
                                                                                                (Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x) = x
                                                                                                @[simp]
                                                                                                theorem Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe {M : Type u_1} [Monoid M] (x : Mˣ) :
                                                                                                (Submonoid.unitsTypeEquivIsUnitSubmonoid x) = x
                                                                                                @[simp]
                                                                                                theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe {M : Type u_1} [AddMonoid M] (x : AddUnits M) :
                                                                                                (AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid x) = x
                                                                                                @[simp]
                                                                                                theorem Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_1} [Monoid M] (x : (IsUnit.submonoid M)) :
                                                                                                (Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x)⁻¹ = (Classical.choose )⁻¹
                                                                                                @[simp]
                                                                                                theorem AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_1} [AddMonoid M] (x : (IsAddUnit.addSubmonoid M)) :
                                                                                                (-AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = (-Classical.choose )
                                                                                                @[simp]
                                                                                                theorem AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_1} [AddMonoid M] (x : (IsAddUnit.addSubmonoid M)) :
                                                                                                (AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = x

                                                                                                The multiplicative equivalence between the type of units of M and the submonoid of unit elements of M.

                                                                                                Equations
                                                                                                • Submonoid.unitsTypeEquivIsUnitSubmonoid = { toFun := fun (x : Mˣ) => x, , invFun := fun (x : (IsUnit.submonoid M)) => IsUnit.unit , left_inv := , right_inv := , map_mul' := }
                                                                                                Instances For
                                                                                                  theorem AddSubmonoid.map_comap_eq {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 : AddSubmonoid N) :
                                                                                                  theorem Submonoid.map_comap_eq {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 : Submonoid N) :
                                                                                                  theorem AddSubmonoid.map_comap_eq_self {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 : AddSubmonoid N} (h : S AddMonoidHom.mrange f) :
                                                                                                  theorem Submonoid.map_comap_eq_self {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 : Submonoid N} (h : S MonoidHom.mrange f) :