# mathlibdocumentation

group_theory.submonoid.operations

# Operations on `submonoid`s #

In this file we define various operations on `submonoid`s and `monoid_hom`s.

## Main definitions #

### Conversion between multiplicative and additive definitions #

• `submonoid.to_add_submonoid`, `submonoid.to_add_submonoid'`, `add_submonoid.to_submonoid`, `add_submonoid.to_submonoid'`: convert between multiplicative and additive submonoids of `M`, `multiplicative M`, and `additive M`. These are stated as `order_iso`s.

### (Commutative) monoid structure on a submonoid #

• `submonoid.to_monoid`, `submonoid.to_comm_monoid`: a submonoid inherits a (commutative) monoid structure.

### Group actions by submonoids #

• `submonoid.mul_action`, `submonoid.distrib_mul_action`: a submonoid inherits (distributive) multiplicative actions.

### Operations on submonoids #

• `submonoid.comap`: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;
• `submonoid.map`: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
• `submonoid.prod`: product of two submonoids `s : submonoid M` and `t : submonoid N` as a submonoid of `M × N`;

### Monoid homomorphisms between submonoid #

• `submonoid.subtype`: embedding of a submonoid into the ambient monoid.
• `submonoid.inclusion`: given two submonoids `S`, `T` such that `S ≤ T`, `S.inclusion T` is the inclusion of `S` into `T` as a monoid homomorphism;
• `mul_equiv.submonoid_congr`: converts a proof of `S = T` into a monoid isomorphism between `S` and `T`.
• `submonoid.prod_equiv`: monoid isomorphism between `s.prod t` and `s × t`;

### Operations on `monoid_hom`s #

• `monoid_hom.mrange`: range of a monoid homomorphism as a submonoid of the codomain;
• `monoid_hom.mker`: kernel of a monoid homomorphism as a submonoid of the domain;
• `monoid_hom.restrict`: restrict a monoid homomorphism to a submonoid;
• `monoid_hom.cod_restrict`: restrict the codomain of a monoid homomorphism to a submonoid;
• `monoid_hom.mrange_restrict`: restrict a monoid homomorphism to its range;

## Tags #

submonoid, range, product, map, comap

### Conversion to/from `additive`/`multiplicative`#

@[simp]
theorem submonoid.to_add_submonoid_apply_coe {M : Type u_1} (S : submonoid M) :
@[simp]
def submonoid.to_add_submonoid {M : Type u_1}  :

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

Equations
@[reducible]
def add_submonoid.to_submonoid' {M : Type u_1}  :

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

theorem submonoid.to_add_submonoid_closure {M : Type u_1} (S : set M) :
theorem add_submonoid.to_submonoid'_closure {M : Type u_1} (S : set (additive M)) :
@[simp]
theorem add_submonoid.to_submonoid_symm_apply_coe {A : Type u_4} (S : submonoid ) :
@[simp]
theorem add_submonoid.to_submonoid_apply_coe {A : Type u_4} (S : add_submonoid A) :
def add_submonoid.to_submonoid {A : Type u_4}  :

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

Equations
@[reducible]
def submonoid.to_add_submonoid' {A : Type u_4}  :

Submonoids of a monoid `multiplicative A` are isomorphic to additive submonoids of `A`.

theorem add_submonoid.to_submonoid_closure {A : Type u_4} (S : set A) :
theorem submonoid.to_add_submonoid'_closure {A : Type u_4} (S : set ) :

### `comap` and `map`#

def submonoid.comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : submonoid N) :

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

Equations
def add_submonoid.comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : add_submonoid N) :

The preimage of an `add_submonoid` along an `add_monoid` homomorphism is an `add_submonoid`.

Equations
@[simp]
theorem submonoid.coe_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S : submonoid N) (f : F) :
@[simp]
theorem add_submonoid.coe_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S : add_submonoid N) (f : F) :
@[simp]
theorem submonoid.mem_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : submonoid N} {f : F} {x : M} :
x f x S
@[simp]
theorem add_submonoid.mem_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : add_submonoid N} {f : F} {x : M} :
x f x S
theorem add_submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} (S : add_submonoid P) (g : N →+ P) (f : M →+ N) :
theorem submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} (S : submonoid P) (g : N →* P) (f : M →* N) :
S) = submonoid.comap (g.comp f) S
@[simp]
theorem submonoid.comap_id {P : Type u_3} (S : submonoid P) :
= S
@[simp]
theorem add_submonoid.comap_id {P : Type u_3} (S : add_submonoid P) :
def submonoid.map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : submonoid M) :

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

Equations
def add_submonoid.map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : add_submonoid M) :

The image of an `add_submonoid` along an `add_monoid` homomorphism is an `add_submonoid`.

Equations
@[simp]
theorem submonoid.coe_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : submonoid M) :
S) = f '' S
@[simp]
theorem add_submonoid.coe_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : add_submonoid M) :
S) = f '' S
@[simp]
theorem add_submonoid.mem_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {S : add_submonoid M} {y : N} :
y ∃ (x : M) (H : x S), f x = y
@[simp]
theorem submonoid.mem_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {S : submonoid M} {y : N} :
y ∃ (x : M) (H : x S), f x = y
theorem submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) {S : submonoid M} {x : M} (hx : x S) :
f x
theorem add_submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) {S : add_submonoid M} {x : M} (hx : x S) :
f x
theorem add_submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : add_submonoid M) (x : S) :
theorem submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (S : submonoid M) (x : S) :
theorem submonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} (S : submonoid M) (g : N →* P) (f : M →* N) :
S) = submonoid.map (g.comp f) S
theorem add_submonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} (S : add_submonoid M) (g : N →+ P) (f : M →+ N) :
theorem add_submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) {S : add_submonoid M} {x : M} :
f x x S
theorem submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) {S : submonoid M} {x : M} :
f x x S
theorem add_submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {S : add_submonoid M} {T : add_submonoid N} :
T S
theorem submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {S : submonoid M} {T : submonoid N} :
T S
theorem submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem add_submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} (S : submonoid M) {F : Type u_4} [mc : N] {T : submonoid N} {f : F} :
S T
theorem add_submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} (S : add_submonoid M) {F : Type u_4} [mc : N] {T : add_submonoid N} {f : F} :
S T
theorem submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} (S : submonoid M) {F : Type u_4} [mc : N] {T : submonoid N} {f : F} :
TS
theorem add_submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} (S : add_submonoid M) {F : Type u_4} [mc : N] {T : add_submonoid N} {f : F} :
TS
theorem submonoid.le_comap_map {M : Type u_1} {N : Type u_2} (S : submonoid M) {F : Type u_4} [mc : N] {f : F} :
S S)
theorem add_submonoid.le_comap_map {M : Type u_1} {N : Type u_2} (S : add_submonoid M) {F : Type u_4} [mc : N] {f : F} :
S
theorem add_submonoid.map_comap_le {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : add_submonoid N} {f : F} :
S
theorem submonoid.map_comap_le {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : submonoid N} {f : F} :
S) S
theorem add_submonoid.monotone_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
theorem submonoid.monotone_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
theorem add_submonoid.monotone_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
theorem submonoid.monotone_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
@[simp]
theorem submonoid.map_comap_map {M : Type u_1} {N : Type u_2} (S : submonoid M) {F : Type u_4} [mc : N] {f : F} :
S)) =
@[simp]
theorem add_submonoid.map_comap_map {M : Type u_1} {N : Type u_2} (S : add_submonoid M) {F : Type u_4} [mc : N] {f : F} :
=
@[simp]
theorem add_submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : add_submonoid N} {f : F} :
@[simp]
theorem submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {S : submonoid N} {f : F} :
S)) =
theorem submonoid.map_sup {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S T : submonoid M) (f : F) :
(S T) =
theorem add_submonoid.map_sup {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S T : add_submonoid M) (f : F) :
(S T) =
theorem submonoid.map_supr {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Sort u_3} (f : F) (s : ι → ) :
(supr s) = ⨆ (i : ι), (s i)
theorem add_submonoid.map_supr {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Sort u_3} (f : F) (s : ι → ) :
(supr s) = ⨆ (i : ι), (s i)
theorem submonoid.comap_inf {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S T : submonoid N) (f : F) :
(S T) =
theorem add_submonoid.comap_inf {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (S T : add_submonoid N) (f : F) :
(S T) =
theorem submonoid.comap_infi {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Sort u_3} (f : F) (s : ι → ) :
(infi s) = ⨅ (i : ι), (s i)
theorem add_submonoid.comap_infi {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Sort u_3} (f : F) (s : ι → ) :
(infi s) = ⨅ (i : ι), (s i)
@[simp]
theorem submonoid.map_bot {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem add_submonoid.map_bot {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem add_submonoid.comap_top {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem submonoid.comap_top {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem add_submonoid.map_id {M : Type u_1} (S : add_submonoid M) :
@[simp]
theorem submonoid.map_id {M : Type u_1} (S : submonoid M) :
= S
def add_submonoid.gci_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :

`map f` and `comap f` form a `galois_coinsertion` when `f` is injective.

Equations
def submonoid.gci_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :

`map f` and `comap f` form a `galois_coinsertion` when `f` is injective.

Equations
theorem add_submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S : add_submonoid M) :
= S
theorem submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S : submonoid M) :
S) = S
theorem add_submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
theorem submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
theorem submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
theorem add_submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
theorem add_submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S T : add_submonoid M) :
= S T
theorem submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S T : submonoid M) :
S T) = S T
theorem submonoid.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.injective f) (S : ι → ) :
(⨅ (i : ι), (S i)) = infi S
theorem add_submonoid.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.injective f) (S : ι → ) :
(⨅ (i : ι), (S i)) = infi S
theorem add_submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S T : add_submonoid M) :
= S T
theorem submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) (S T : submonoid M) :
S T) = S T
theorem submonoid.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.injective f) (S : ι → ) :
(⨆ (i : ι), (S i)) = supr S
theorem add_submonoid.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.injective f) (S : ι → ) :
(⨆ (i : ι), (S i)) = supr S
theorem submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) {S T : submonoid M} :
S T
theorem add_submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) {S T : add_submonoid M} :
S T
theorem add_submonoid.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
theorem submonoid.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.injective f) :
def submonoid.gi_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :

`map f` and `comap f` form a `galois_insertion` when `f` is surjective.

Equations
def add_submonoid.gi_map_comap {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :

`map f` and `comap f` form a `galois_insertion` when `f` is surjective.

Equations
theorem add_submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S : add_submonoid N) :
= S
theorem submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S : submonoid N) :
S) = S
theorem submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
theorem add_submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
theorem add_submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
theorem submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
theorem add_submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S T : add_submonoid N) :
= S T
theorem submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S T : submonoid N) :
S T) = S T
theorem add_submonoid.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.surjective f) (S : ι → ) :
(⨅ (i : ι), (S i)) = infi S
theorem submonoid.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.surjective f) (S : ι → ) :
(⨅ (i : ι), (S i)) = infi S
theorem submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S T : submonoid N) :
S T) = S T
theorem add_submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) (S T : add_submonoid N) :
= S T
theorem submonoid.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.surjective f) (S : ι → ) :
(⨆ (i : ι), (S i)) = supr S
theorem add_submonoid.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {ι : Type u_5} {f : F} (hf : function.surjective f) (S : ι → ) :
(⨆ (i : ι), (S i)) = supr S
theorem add_submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) {S T : add_submonoid N} :
S T
theorem submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) {S T : submonoid N} :
S T
theorem add_submonoid.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
theorem submonoid.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} (hf : function.surjective f) :
@[protected, instance]
def one_mem_class.has_one {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_one M₁] [hA : M₁] (S' : A) :

A submonoid of a monoid inherits a 1.

Equations
@[protected, instance]
def zero_mem_class.has_zero {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_zero M₁] [hA : M₁] (S' : A) :

An `add_submonoid` of an `add_monoid` inherits a zero.

Equations
@[simp, norm_cast]
theorem zero_mem_class.coe_zero {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_zero M₁] [hA : M₁] (S' : A) :
0 = 0
@[simp, norm_cast]
theorem one_mem_class.coe_one {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_one M₁] [hA : M₁] (S' : A) :
1 = 1
@[simp, norm_cast]
theorem zero_mem_class.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_zero M₁] [hA : M₁] {S' : A} {x : S'} :
x = 0 x = 0
@[simp, norm_cast]
theorem one_mem_class.coe_eq_one {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_one M₁] [hA : M₁] {S' : A} {x : S'} :
x = 1 x = 1
theorem zero_mem_class.zero_def {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_zero M₁] [hA : M₁] (S' : A) :
0 = 0, _⟩
theorem one_mem_class.one_def {A : Type u_4} {M₁ : Type u_5} [ M₁] [has_one M₁] [hA : M₁] (S' : A) :
1 = 1, _⟩
@[protected, instance]
def add_submonoid_class.has_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an `add_monoid` inherits a scalar multiplication.

Equations
@[protected, instance]
def submonoid_class.has_pow {M : Type u_1} [monoid M] {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of a monoid inherits a power operator.

Equations
@[simp, norm_cast]
theorem add_submonoid_class.coe_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [ M] [ M] {S : A} (x : S) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem submonoid_class.coe_pow {M : Type u_1} [monoid M] {A : Type u_2} [ M] [ M] {S : A} (x : S) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem add_submonoid_class.mk_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [ M] [ M] {S : A} (x : M) (hx : x S) (n : ) :
n x, hx⟩ = n x, _⟩
@[simp]
theorem submonoid_class.mk_pow {M : Type u_1} [monoid M] {A : Type u_2} [ M] [ M] {S : A} (x : M) (hx : x S) (n : ) :
x, hx⟩ ^ n = x ^ n, _⟩
@[protected, instance]
def add_submonoid_class.to_add_zero_class {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an unital additive magma inherits an unital additive magma structure.

Equations
@[protected, instance]
def submonoid_class.to_mul_one_class {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

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

Equations
@[protected, instance]
def submonoid_class.to_monoid {M : Type u_1} [monoid M] {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of a monoid inherits a monoid structure.

Equations
@[protected, instance]
def add_submonoid_class.to_add_monoid {M : Type u_1} [add_monoid M] {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an `add_monoid` inherits an `add_monoid` structure.

Equations
@[protected, instance]
def submonoid_class.to_comm_monoid {M : Type u_1} [comm_monoid M] {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of a `comm_monoid` is a `comm_monoid`.

Equations
@[protected, instance]
def add_submonoid_class.to_add_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an `add_comm_monoid` is an `add_comm_monoid`.

Equations
@[protected, instance]
def add_submonoid_class.to_ordered_add_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an `ordered_add_comm_monoid` is an `ordered_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid_class.to_ordered_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of an `ordered_comm_monoid` is an `ordered_comm_monoid`.

Equations
@[protected, instance]
def add_submonoid_class.to_linear_ordered_add_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of a `linear_ordered_add_comm_monoid` is a `linear_ordered_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid_class.to_linear_ordered_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of a `linear_ordered_comm_monoid` is a `linear_ordered_comm_monoid`.

Equations
@[protected, instance]
def add_submonoid_class.to_ordered_cancel_add_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is an `ordered_cancel_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid_class.to_ordered_cancel_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`.

Equations
@[protected, instance]
def submonoid_class.to_linear_ordered_cancel_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

A submonoid of a `linear_ordered_cancel_comm_monoid` is a `linear_ordered_cancel_comm_monoid`.

Equations
@[protected, instance]
def add_submonoid_class.to_linear_ordered_cancel_add_comm_monoid {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_submonoid` of a `linear_ordered_cancel_add_comm_monoid` is a `linear_ordered_cancel_add_comm_monoid`.

Equations
def submonoid_class.subtype {M : Type u_1} {A : Type u_4} [ M] [hA : M] (S' : A) :
S' →* M

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

Equations
def add_submonoid_class.subtype {M : Type u_1} {A : Type u_4} [ M] [hA : M] (S' : A) :
S' →+ M

The natural monoid hom from an `add_submonoid` of `add_monoid` `M` to `M`.

Equations
@[simp]
theorem add_submonoid_class.coe_subtype {M : Type u_1} {A : Type u_4} [ M] [hA : M] (S' : A) :
@[simp]
theorem submonoid_class.coe_subtype {M : Type u_1} {A : Type u_4} [ M] [hA : M] (S' : A) :
@[protected, instance]
def submonoid.has_mul {M : Type u_1} (S : submonoid M) :

A submonoid of a monoid inherits a multiplication.

Equations
@[protected, instance]
def add_submonoid.has_add {M : Type u_1} (S : add_submonoid M) :

An `add_submonoid` of an `add_monoid` inherits an addition.

Equations
@[protected, instance]
def submonoid.has_one {M : Type u_1} (S : submonoid M) :

A submonoid of a monoid inherits a 1.

Equations
@[protected, instance]
def add_submonoid.has_zero {M : Type u_1} (S : add_submonoid M) :

An `add_submonoid` of an `add_monoid` inherits a zero.

Equations
@[simp, norm_cast]
theorem submonoid.coe_mul {M : Type u_1} (S : submonoid M) (x y : S) :
(x * y) = x * y
@[simp, norm_cast]
theorem add_submonoid.coe_add {M : Type u_1} (S : add_submonoid M) (x y : S) :
(x + y) = x + y
@[simp, norm_cast]
theorem add_submonoid.coe_zero {M : Type u_1} (S : add_submonoid M) :
0 = 0
@[simp, norm_cast]
theorem submonoid.coe_one {M : Type u_1} (S : submonoid M) :
1 = 1
@[simp]
theorem submonoid.mk_mul_mk {M : Type u_1} (S : submonoid M) (x y : M) (hx : x S) (hy : y S) :
x, hx⟩ * y, hy⟩ = x * y, _⟩
@[simp]
theorem add_submonoid.mk_add_mk {M : Type u_1} (S : add_submonoid M) (x y : M) (hx : x S) (hy : y S) :
x, hx⟩ + y, hy⟩ = x + y, _⟩
theorem submonoid.mul_def {M : Type u_1} (S : submonoid M) (x y : S) :
x * y = x * y, _⟩
theorem add_submonoid.add_def {M : Type u_1} (S : add_submonoid M) (x y : S) :
x + y = x + y, _⟩
theorem submonoid.one_def {M : Type u_1} (S : submonoid M) :
1 = 1, _⟩
theorem add_submonoid.zero_def {M : Type u_1} (S : add_submonoid M) :
0 = 0, _⟩
@[protected, instance]
def add_submonoid.to_add_zero_class {M : Type u_1} (S : add_submonoid M) :

An `add_submonoid` of an unital additive magma inherits an unital additive magma structure.

Equations
@[protected, instance]
def submonoid.to_mul_one_class {M : Type u_1} (S : submonoid M) :

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

Equations
@[protected]
theorem submonoid.pow_mem {M : Type u_1} [monoid M] (S : submonoid M) {x : M} (hx : x S) (n : ) :
x ^ n S
@[protected]
theorem add_submonoid.nsmul_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {x : M} (hx : x S) (n : ) :
n x S
@[simp, norm_cast]
theorem add_submonoid.coe_nsmul {M : Type u_1} [add_monoid M] {S : add_submonoid M} (x : S) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem submonoid.coe_pow {M : Type u_1} [monoid M] {S : submonoid M} (x : S) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def submonoid.to_monoid {M : Type u_1} [monoid M] (S : submonoid M) :

A submonoid of a monoid inherits a monoid structure.

Equations
@[protected, instance]

An `add_submonoid` of an `add_monoid` inherits an `add_monoid` structure.

Equations
@[protected, instance]
def add_submonoid.to_add_comm_monoid {M : Type u_1} (S : add_submonoid M) :

An `add_submonoid` of an `add_comm_monoid` is an `add_comm_monoid`.

Equations
@[protected, instance]
def submonoid.to_comm_monoid {M : Type u_1} [comm_monoid M] (S : submonoid M) :

A submonoid of a `comm_monoid` is a `comm_monoid`.

Equations
@[protected, instance]

An `add_submonoid` of an `ordered_add_comm_monoid` is an `ordered_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid.to_ordered_comm_monoid {M : Type u_1} (S : submonoid M) :

A submonoid of an `ordered_comm_monoid` is an `ordered_comm_monoid`.

Equations
@[protected, instance]

An `add_submonoid` of a `linear_ordered_add_comm_monoid` is a `linear_ordered_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid.to_linear_ordered_comm_monoid {M : Type u_1} (S : submonoid M) :

A submonoid of a `linear_ordered_comm_monoid` is a `linear_ordered_comm_monoid`.

Equations
@[protected, instance]

An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is an `ordered_cancel_add_comm_monoid`.

Equations
@[protected, instance]
def submonoid.to_ordered_cancel_comm_monoid {M : Type u_1} (S : submonoid M) :

A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`.

Equations
@[protected, instance]

An `add_submonoid` of a `linear_ordered_cancel_add_comm_monoid` is a `linear_ordered_cancel_add_comm_monoid`.

Equations
@[protected, instance]

A submonoid of a `linear_ordered_cancel_comm_monoid` is a `linear_ordered_cancel_comm_monoid`.

Equations
def add_submonoid.subtype {M : Type u_1} (S : add_submonoid M) :

The natural monoid hom from an `add_submonoid` of `add_monoid` `M` to `M`.

Equations
def submonoid.subtype {M : Type u_1} (S : submonoid M) :

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

Equations
@[simp]
theorem add_submonoid.coe_subtype {M : Type u_1} (S : add_submonoid M) :
@[simp]
theorem submonoid.coe_subtype {M : Type u_1} (S : submonoid M) :
@[simp]
theorem add_submonoid.top_equiv_symm_apply_coe {M : Type u_1} (x : M) :
= x
def submonoid.top_equiv {M : Type u_1}  :

The top submonoid is isomorphic to the monoid.

Equations
@[simp]
theorem submonoid.top_equiv_symm_apply_coe {M : Type u_1} (x : M) :
@[simp]
theorem add_submonoid.top_equiv_apply {M : Type u_1} (x : ) :
@[simp]
theorem submonoid.top_equiv_apply {M : Type u_1} (x : ) :
def add_submonoid.top_equiv {M : Type u_1}  :

The top additive submonoid is isomorphic to the additive monoid.

Equations
@[simp]
theorem submonoid.top_equiv_to_monoid_hom {M : Type u_1}  :
@[simp]
theorem add_submonoid.top_equiv_to_add_monoid_hom {M : Type u_1}  :
noncomputable def add_submonoid.equiv_map_of_injective {M : Type u_1} {N : Type u_2} (S : add_submonoid M) (f : M →+ N) (hf : function.injective f) :

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

Equations
noncomputable def submonoid.equiv_map_of_injective {M : Type u_1} {N : Type u_2} (S : submonoid M) (f : M →* N) (hf : function.injective f) :

A submonoid is isomorphic to its image under an injective function

Equations
@[simp]
theorem add_submonoid.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} (S : add_submonoid M) (f : M →+ N) (hf : function.injective f) (x : S) :
( hf) x) = f x
@[simp]
theorem submonoid.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} (S : submonoid M) (f : M →* N) (hf : function.injective f) (x : S) :
( hf) x) = f x
@[simp]
theorem submonoid.closure_closure_coe_preimage {M : Type u_1} {s : set M} :
@[simp]
theorem add_submonoid.closure_closure_coe_preimage {M : Type u_1} {s : set M} :
def submonoid.prod {M : Type u_1} {N : Type u_2} (s : submonoid M) (t : submonoid N) :

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

Equations
def add_submonoid.prod {M : Type u_1} {N : Type u_2} (s : add_submonoid M) (t : add_submonoid N) :

Given `add_submonoid`s `s`, `t` of `add_monoid`s `A`, `B` respectively, `s × t` as an `add_submonoid` of `A × B`.

Equations
theorem add_submonoid.coe_prod {M : Type u_1} {N : Type u_2} (s : add_submonoid M) (t : add_submonoid N) :
(s.prod t) = s ×ˢ t
theorem submonoid.coe_prod {M : Type u_1} {N : Type u_2} (s : submonoid M) (t : submonoid N) :
(s.prod t) = s ×ˢ t
theorem submonoid.mem_prod {M : Type u_1} {N : Type u_2} {s : submonoid M} {t : submonoid N} {p : M × N} :
p s.prod t p.fst s p.snd t
theorem add_submonoid.mem_prod {M : Type u_1} {N : Type u_2} {s : add_submonoid M} {t : add_submonoid N} {p : M × N} :
p s.prod t p.fst s p.snd t
theorem add_submonoid.prod_mono {M : Type u_1} {N : Type u_2} {s₁ s₂ : add_submonoid M} {t₁ t₂ : add_submonoid 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} {s₁ s₂ : submonoid M} {t₁ t₂ : submonoid N} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem add_submonoid.prod_top {M : Type u_1} {N : Type u_2} (s : add_submonoid M) :
theorem submonoid.prod_top {M : Type u_1} {N : Type u_2} (s : submonoid M) :
s.prod = s
theorem submonoid.top_prod {M : Type u_1} {N : Type u_2} (s : submonoid N) :
.prod s = s
theorem add_submonoid.top_prod {M : Type u_1} {N : Type u_2} (s : add_submonoid N) :
@[simp]
theorem add_submonoid.top_prod_top {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem submonoid.top_prod_top {M : Type u_1} {N : Type u_2}  :
theorem add_submonoid.bot_sum_bot {M : Type u_1} {N : Type u_2}  :
theorem submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2}  :
def submonoid.prod_equiv {M : Type u_1} {N : Type u_2} (s : submonoid M) (t : submonoid N) :

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

Equations
def add_submonoid.prod_equiv {M : Type u_1} {N : Type u_2} (s : add_submonoid M) (t : add_submonoid N) :

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

Equations
theorem add_submonoid.map_inl {M : Type u_1} {N : Type u_2} (s : add_submonoid M) :
theorem submonoid.map_inl {M : Type u_1} {N : Type u_2} (s : submonoid M) :
s = s.prod
theorem submonoid.map_inr {M : Type u_1} {N : Type u_2} (s : submonoid N) :
s = .prod s
theorem add_submonoid.map_inr {M : Type u_1} {N : Type u_2} (s : add_submonoid N) :
@[simp]
theorem submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} (s : submonoid M) (t : submonoid N) :
@[simp]
theorem add_submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} (s : add_submonoid M) (t : add_submonoid N) :
theorem add_submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} {f : M ≃+ N} {K : add_submonoid M} {x : N} :
(f.symm) x K
theorem submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} {f : M ≃* N} {K : submonoid M} {x : N} :
(f.symm) x K
theorem add_submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} (f : M ≃+ N) (K : add_submonoid M) :
theorem submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} (f : M ≃* N) (K : submonoid M) :
theorem submonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} (f : N ≃* M) (K : submonoid M) :
theorem add_submonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} (f : N ≃+ M) (K : add_submonoid M) :
@[simp]
theorem submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} (f : M ≃* N) :
@[simp]
theorem add_submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} (f : M ≃+ N) :
theorem add_submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} {s : add_submonoid M} {t : add_submonoid N} {u : add_submonoid (M × N)} :
u s.prod t s t
theorem submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} {s : submonoid M} {t : submonoid N} {u : submonoid (M × N)} :
u s.prod t u s u t
theorem submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} {s : submonoid M} {t : submonoid N} {u : submonoid (M × N)} :
s.prod t u s u t u
theorem add_submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} {s : add_submonoid M} {t : add_submonoid N} {u : add_submonoid (M × N)} :
s.prod t u u u

For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism `f` is a subobject of the codomain. When this is the case, it is useful to define the range of a morphism in such a way that the underlying carrier set of the range subobject is definitionally `set.range f`. In particular this means that the types `↥(set.range f)` and `↥f.range` are interchangeable without proof obligations.

A convenient candidate definition for range which is mathematically correct is `map ⊤ f`, just as `set.range` could have been defined as `f '' set.univ`. However, this lacks the desired definitional convenience, in that it both does not match `set.range`, and that it introduces a redudant `x ∈ ⊤` term which clutters proofs. In such a case one may resort to the `copy` pattern. A `copy` function converts the definitional problem for the carrier set of a subobject into a one-off propositional proof obligation which one discharges while writing the definition of the definitionally convenient range (the parameter `hs` in the example below).

A good example is the case of a morphism of monoids. A convenient definition for `monoid_hom.mrange` would be `(⊤ : submonoid M).map f`. However since this lacks the required definitional convenience, we first define `submonoid.copy` as follows:

``````protected def copy (S : submonoid M) (s : set M) (hs : s = S) : submonoid M :=
{ carrier  := s,
one_mem' := hs.symm ▸ S.one_mem',
mul_mem' := hs.symm ▸ S.mul_mem' }
``````

and then finally define:

``````def mrange (f : M →* N) : submonoid N :=
((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm
``````
def monoid_hom.mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :

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

Equations
Instances for `↥monoid_hom.mrange`
def add_monoid_hom.mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :

The range of an `add_monoid_hom` is an `add_submonoid`.

Equations
Instances for `↥add_monoid_hom.mrange`
@[simp]
theorem monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem add_monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem add_monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {y : N} :
∃ (x : M), f x = y
@[simp]
theorem monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} {y : N} :
∃ (x : M), f x = y
theorem monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem add_monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem add_monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →+ P) (f : M →+ N) :
theorem monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →* P) (f : M →* N) :
theorem add_monoid_hom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
theorem monoid_hom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] {f : F} :
theorem add_monoid_hom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (hf : function.surjective f) :

The range of a surjective `add_monoid` hom is the whole of the codomain.

theorem monoid_hom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (hf : function.surjective f) :

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

theorem monoid_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (s : set N) :
theorem add_monoid_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (s : set N) :
theorem add_monoid_hom.map_mclosure {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (s : set M) :

The image under an `add_monoid` hom of the `add_submonoid` generated by a set equals the `add_submonoid` generated by the image of the set.

theorem monoid_hom.map_mclosure {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) (s : set M) :

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

def add_monoid_hom.restrict {M : Type u_1} {N : Type u_2} {S : Type u_3} [ M] [ M] (f : M →+ N) (s : S) :

Restriction of an add_monoid hom to an `add_submonoid` of the domain.

Equations
def monoid_hom.restrict {M : Type u_1} {N : Type u_2} {S : Type u_3} [ M] [ M] (f : M →* N) (s : S) :

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

Equations
@[simp]
theorem add_monoid_hom.restrict_apply {M : Type u_1} {N : Type u_2} {S : Type u_3} [ M] [ M] (f : M →+ N) (s : S) (x : s) :
(f.restrict s) x = f x
@[simp]
theorem monoid_hom.restrict_apply {M : Type u_1} {N : Type u_2} {S : Type u_3} [ M] [ M] (f : M →* N) (s : S) (x : s) :
(f.restrict s) x = f x
@[simp]
theorem monoid_hom.cod_restrict_apply {M : Type u_1} {N : Type u_2} {S : Type u_3} [ N] [ N] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
(f.cod_restrict s h) n = f n, _⟩
def add_monoid_hom.cod_restrict {M : Type u_1} {N : Type u_2} {S : Type u_3} [ N] [ N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) :

Restriction of an `add_monoid` hom to an `add_submonoid` of the codomain.

Equations
def monoid_hom.cod_restrict {M : Type u_1} {N : Type u_2} {S : Type u_3} [ N] [ N] (f : M →* N) (s : S) (h : ∀ (x : M), f x s) :

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

Equations
@[simp]
theorem add_monoid_hom.cod_restrict_apply {M : Type u_1} {N : Type u_2} {S : Type u_3} [ N] [ N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x s) (n : M) :
(f.cod_restrict s h) n = f n, _⟩
def add_monoid_hom.mrange_restrict {M : Type u_1} {N : Type u_2} (f : M →+ N) :

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

Equations
def monoid_hom.mrange_restrict {M : Type u_1} {N : Type u_2} (f : M →* N) :
M →*

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

Equations
@[simp]
theorem add_monoid_hom.coe_mrange_restrict {M : Type u_1} {N : Type u_2} (f : M →+ N) (x : M) :
@[simp]
theorem monoid_hom.coe_mrange_restrict {M : Type u_1} {N : Type u_2} (f : M →* N) (x : M) :
theorem add_monoid_hom.mrange_restrict_surjective {M : Type u_1} {N : Type u_2} (f : M →+ N) :
theorem monoid_hom.mrange_restrict_surjective {M : Type u_1} {N : Type u_2} (f : M →* N) :
def monoid_hom.mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :

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

Equations
def add_monoid_hom.mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :

The additive kernel of an `add_monoid` homomorphism is the `add_submonoid` of elements such that `f x = 0`

Equations
theorem monoid_hom.mem_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) {x : M} :
f x = 1
theorem add_monoid_hom.mem_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) {x : M} :
f x = 0
theorem monoid_hom.coe_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem add_monoid_hom.coe_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
= f ⁻¹' {0}
@[protected, instance]
def add_monoid_hom.decidable_mem_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] [decidable_eq N] (f : F) :
Equations
@[protected, instance]
def monoid_hom.decidable_mem_mker {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] [decidable_eq N] (f : F) :
decidable_pred (λ (_x : M), _x monoid_hom.mker f)
Equations
theorem add_monoid_hom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →+ P) (f : M →+ N) :
theorem monoid_hom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →* P) (f : M →* N) :
@[simp]
theorem add_monoid_hom.comap_bot' {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
@[simp]
theorem monoid_hom.comap_bot' {M : Type u_1} {N : Type u_2} {F : Type u_4} [mc : N] (f : F) :
theorem monoid_hom.range_restrict_mker {M : Type u_1} {N : Type u_2} (f : M →* N) :
theorem add_monoid_hom.range_restrict_mker {M : Type u_1} {N : Type u_2} (f : M →+ N) :
@[simp]
theorem add_monoid_hom.mker_zero {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem monoid_hom.mker_one {M : Type u_1} {N : Type u_2}  :
theorem monoid_hom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [mul_one_class M'] [mul_one_class N'] (f : M →* N) (g : M' →* N') (S : submonoid N) (S' : submonoid N') :
submonoid.comap (f.prod_map g) (S.prod S') = S).prod S')
theorem add_monoid_hom.sum_map_comap_sum' {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [add_zero_class M'] [add_zero_class N'] (f : M →+ N) (g : M' →+ N') (S : add_submonoid N) (S' : add_submonoid N') :
(S.prod S') = S).prod S')
theorem add_monoid_hom.mker_sum_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [add_zero_class M'] [add_zero_class N'] (f : M →+ N) (g : M' →+ N') :
theorem monoid_hom.mker_prod_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [mul_one_class M'] [mul_one_class N'] (f : M →* N) (g : M' →* N') :
@[simp]
theorem monoid_hom.mker_inl {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_monoid_hom.mker_inl {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_monoid_hom.mker_inr {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem monoid_hom.mker_inr {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem monoid_hom.submonoid_comap_apply_coe {M : Type u_1} {N : Type u_2} (f : M →* N) (N' : submonoid N) (x : N')) :
def add_monoid_hom.add_submonoid_comap {M : Type u_1} {N : Type u_2} (f : M →+ N) (N' : add_submonoid N) :
N') →+ N'

the `add_monoid_hom` from the preimage of an additive submonoid to itself.

Equations
def monoid_hom.submonoid_comap {M : Type u_1} {N : Type u_2} (f : M →* N) (N' : submonoid N) :
N') →* N'

The `monoid_hom` from the preimage of a submonoid to itself.

Equations
@[simp]
theorem add_monoid_hom.add_submonoid_comap_apply_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) (N' : add_submonoid N) (x : N')) :
def add_monoid_hom.add_submonoid_map {M : Type u_1} {N : Type u_2} (f : M →+ N) (M' : add_submonoid M) :
M' →+ M')

the `add_monoid_hom` from an additive submonoid to its image. See `add_equiv.add_submonoid_map` for a variant for `add_equiv`s.

Equations
def monoid_hom.submonoid_map {M : Type u_1} {N : Type u_2} (f : M →* N) (M' : submonoid M) :
M' →* M')

The `monoid_hom` from a submonoid to its image. See `mul_equiv.submonoid_map` for a variant for `mul_equiv`s.

Equations
@[simp]
theorem monoid_hom.submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} (f : M →* N) (M' : submonoid M) (x : M') :
@[simp]
theorem add_monoid_hom.add_submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) (M' : add_submonoid M) (x : M') :
theorem add_monoid_hom.add_submonoid_map_surjective {M : Type u_1} {N : Type u_2} (f : M →+ N) (M' : add_submonoid M) :
theorem monoid_hom.submonoid_map_surjective {M : Type u_1} {N : Type u_2} (f : M →* N) (M' : submonoid M) :
theorem submonoid.mrange_inl {M : Type u_1} {N : Type u_2}  :
theorem add_submonoid.mrange_inl {M : Type u_1} {N : Type u_2}  :
theorem submonoid.mrange_inr {M : Type u_1} {N : Type u_2}  :
theorem add_submonoid.mrange_inr {M : Type u_1} {N : Type u_2}  :
theorem add_submonoid.mrange_inl' {M : Type u_1} {N : Type u_2}  :
theorem submonoid.mrange_inl' {M : Type u_1} {N : Type u_2}  :
theorem submonoid.mrange_inr' {M : Type u_1} {N : Type u_2}  :
theorem add_submonoid.mrange_inr' {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem submonoid.mrange_fst {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_submonoid.mrange_fst {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem submonoid.mrange_snd {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_submonoid.mrange_snd {M : Type u_1} {N : Type u_2}  :
theorem submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} {s : submonoid M} {t : submonoid N} :
s.prod t = s = t =
theorem add_submonoid.sum_eq_bot_iff {M : Type u_1} {N : Type u_2} {s : add_submonoid M} {t : add_submonoid N} :
s.prod t = s = t =
theorem submonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} {s : submonoid M} {t : submonoid N} :
s.prod t = s = t =
theorem add_submonoid.sum_eq_top_iff {M : Type u_1} {N : Type u_2} {s : add_submonoid M} {t : add_submonoid N} :
s.prod t = s = t =
@[simp]
theorem submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2}  :
def submonoid.inclusion {M : Type u_1} {S T : submonoid M} (h : S T) :

The monoid hom associated to an inclusion of submonoids.

Equations
def add_submonoid.inclusion {M : Type u_1} {S T : add_submonoid M} (h : S T) :

The `add_monoid` hom associated to an inclusion of submonoids.

Equations
@[simp]
theorem add_submonoid.range_subtype {M : Type u_1} (s : add_submonoid M) :
@[simp]
theorem submonoid.range_subtype {M : Type u_1} (s : submonoid M) :
theorem add_submonoid.eq_top_iff' {M : Type u_1} (S : add_submonoid M) :
S = ∀ (x : M), x S
theorem submonoid.eq_top_iff' {M : Type u_1} (S : submonoid M) :
S = ∀ (x : M), x S
theorem submonoid.eq_bot_iff_forall {M : Type u_1} (S : submonoid M) :
S = ∀ (x : M), x Sx = 1
theorem add_submonoid.eq_bot_iff_forall {M : Type u_1} (S : add_submonoid M) :
S = ∀ (x : M), x Sx = 0
theorem submonoid.nontrivial_iff_exists_ne_one {M : Type u_1} (S : submonoid M) :
∃ (x : M) (H : x S), x 1
theorem add_submonoid.nontrivial_iff_exists_ne_zero {M : Type u_1} (S : add_submonoid M) :
∃ (x : M) (H : x S), x 0
theorem submonoid.bot_or_nontrivial {M : Type u_1} (S : submonoid M) :
S =

A submonoid is either the trivial submonoid or nontrivial.

theorem add_submonoid.bot_or_nontrivial {M : Type u_1} (S : add_submonoid M) :
S =

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

theorem submonoid.bot_or_exists_ne_one {M : Type u_1} (S : submonoid M) :
S = ∃ (x : M) (H : x S), x 1

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

theorem add_submonoid.bot_or_exists_ne_zero {M : Type u_1} (S : add_submonoid M) :
S = ∃ (x : M) (H : x S), x 0

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

def mul_equiv.submonoid_congr {M : Type u_1} {S T : submonoid M} (h : S = T) :

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

Equations
def add_equiv.add_submonoid_congr {M : Type u_1} {S T : add_submonoid M} (h : S = T) :

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

Equations
def mul_equiv.of_left_inverse' {M : Type u_1} {N : Type u_2} (f : M →* N) {g : N → M} (h : f) :
M ≃*

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 `monoid_hom.mrange_restrict`.

Equations
@[simp]
theorem add_equiv.of_left_inverse'_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) {g : N → M} (h : f) (ᾰ : M) :
= (f.mrange_restrict) ᾰ
@[simp]
theorem mul_equiv.of_left_inverse'_apply {M : Type u_1} {N : Type u_2} (f : M →* N) {g : N → M} (h : f) (ᾰ : M) :
= (f.mrange_restrict) ᾰ
@[simp]
theorem mul_equiv.of_left_inverse'_symm_apply {M : Type u_1} {N : Type u_2} (f : M →* N) {g : N → M} (h : f) (ᾰ : ) :
.symm) = g
def add_equiv.of_left_inverse' {M : Type u_1} {N : Type u_2} (f : M →+ N) {g : N → M} (h : 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 `add_monoid_hom.mrange_restrict`.

Equations
@[simp]
theorem add_equiv.of_left_inverse'_symm_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) {g : N → M} (h : f) (ᾰ : ) :
.symm) = g
@[simp]
theorem mul_equiv.submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} (e : M ≃* N) (S : submonoid M) (x : S) :
@[simp]
theorem mul_equiv.submonoid_map_symm_apply_coe {M : Type u_1} {N : Type u_2} (e : M ≃* N) (S : submonoid M) (x : ) :
@[simp]
theorem add_equiv.add_submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} (e : M ≃+ N) (S : add_submonoid M) (x : S) :
@[simp]
theorem add_equiv.add_submonoid_map_symm_apply_coe {M : Type u_1} {N : Type u_2} (e : M ≃+ N) (S : add_submonoid M) (x : ) :
def add_equiv.add_submonoid_map {M : Type u_1} {N : Type u_2} (e : M ≃+ N) (S : add_submonoid M) :

An `add_equiv` `φ` between two additive monoids `M` and `N` induces an `add_equiv` between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See `add_monoid_hom.add_submonoid_map` for a variant for `add_monoid_hom`s.

Equations
def mul_equiv.submonoid_map {M : Type u_1} {N : Type u_2} (e : M ≃* N) (S : submonoid M) :

A `mul_equiv` `φ` between two monoids `M` and `N` induces a `mul_equiv` between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See `monoid_hom.submonoid_map` for a variant for `monoid_hom`s.

Equations

### Actions by `submonoid`s #

These instances tranfer 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.to_mul_action`, enabling `s • m` as an alias for `↑s * m`.

@[protected, instance]
def add_submonoid.has_vadd {M' : Type u_4} {α : Type u_5} [add_zero_class M'] [has_vadd M' α] (S : add_submonoid M') :
α
Equations
@[protected, instance]
def submonoid.has_smul {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] (S : submonoid M') :
α
Equations
@[protected, instance]
def add_submonoid.vadd_comm_class_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [add_zero_class M'] [has_vadd M' β] [ β] [ α β] (S : add_submonoid M') :
β
@[protected, instance]
def submonoid.smul_comm_class_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [has_smul M' β] [ β] [ α β] (S : submonoid M') :
β
@[protected, instance]
def add_submonoid.vadd_comm_class_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [add_zero_class M'] [ β] [has_vadd M' β] [ M' β] (S : add_submonoid M') :
β
@[protected, instance]
def submonoid.smul_comm_class_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [ β] [has_smul M' β] [ M' β] (S : submonoid M') :
β
@[protected, instance]
def submonoid.is_scalar_tower {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [ β] [has_smul M' α] [has_smul M' β] [ α β] (S : submonoid M') :
β

Note that this provides `is_scalar_tower S M' M'` which is needed by `smul_mul_assoc`.

theorem submonoid.smul_def {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] {S : submonoid M'} (g : S) (m : α) :
g m = g m
theorem add_submonoid.vadd_def {M' : Type u_4} {α : Type u_5} [add_zero_class M'] [has_vadd M' α] {S : add_submonoid M'} (g : S) (m : α) :
g +ᵥ m = g +ᵥ m
@[protected, instance]
def submonoid.has_faithful_smul {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] [ α] (S : submonoid M') :
@[protected, instance]
def submonoid.mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [ α] (S : submonoid M') :
α

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

Equations
@[protected, instance]
def add_submonoid.add_action {M' : Type u_4} {α : Type u_5} [add_monoid M'] [ α] (S : add_submonoid M') :
α

The additive action by an add_submonoid is the action by the underlying add_monoid.

Equations
@[protected, instance]
def submonoid.distrib_mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [add_monoid α] [ α] (S : submonoid M') :

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

Equations
@[protected, instance]
def submonoid.mul_distrib_mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [monoid α] [ α] (S : submonoid M') :

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

Equations