mathlib documentation

group_theory.submonoid.operations

Operations on submonoids #

In this file we define various operations on submonoids and monoid_homs.

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) monoid structure on a submonoid #

Operations on submonoids #

Monoid homomorphisms between submonoid #

Operations on monoid_homs #

Tags #

submonoid, range, product, map, comap

Conversion to/from additive/multiplicative #

Map from submonoids of monoid M to add_submonoids of additive M.

Equations

Map from add_submonoids of additive M to submonoids of M.

Equations

Map from add_submonoids of M to submonoids of multiplicative M.

Equations

Map from submonoids of M to add_submonoids of add_monoid M.

Equations

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

Equations

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

Equations

comap and map #

def submonoid.comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (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} [add_zero_class M] [add_zero_class N] (f : M →+ N) (S : add_submonoid N) :

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

@[simp]
theorem submonoid.coe_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid N) (f : M →* N) :
@[simp]
theorem add_submonoid.coe_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid N) (f : M →+ N) :
@[simp]
theorem submonoid.mem_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {S : submonoid N} {f : M →* N} {x : M} :
@[simp]
theorem add_submonoid.mem_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {S : add_submonoid N} {f : M →+ N} {x : M} :
theorem add_submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (S : submonoid P) (g : N →* P) (f : M →* N) :
@[simp]
theorem submonoid.comap_id {P : Type u_3} [mul_one_class P] (S : submonoid P) :
@[simp]
def submonoid.map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (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} [add_zero_class M] [add_zero_class N] (f : M →+ N) (S : add_submonoid M) :

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

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

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

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

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

Equations
theorem submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f : M →* N} (hf : function.surjective f) (S : submonoid N) :
theorem submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f : M →* N} (hf : function.surjective f) (S T : submonoid N) :
theorem submonoid.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {ι : Type u_4} {f : M →* N} (hf : function.surjective f) (S : ι → submonoid N) :
submonoid.map f (⨅ (i : ι), submonoid.comap f (S i)) = infi S
theorem submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f : M →* N} (hf : function.surjective f) (S T : submonoid N) :
theorem submonoid.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {ι : Type u_4} {f : M →* N} (hf : function.surjective f) (S : ι → submonoid N) :
submonoid.map f (⨆ (i : ι), submonoid.comap f (S i)) = supr S
theorem submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f : M →* N} (hf : function.surjective f) {S T : submonoid N} :
@[instance]
def submonoid.has_mul {M : Type u_1} [mul_one_class M] (S : submonoid M) :

A submonoid of a monoid inherits a multiplication.

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

An add_submonoid of an add_monoid inherits an addition.

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

A submonoid of a monoid inherits a 1.

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

An add_submonoid of an add_monoid inherits a zero.

@[simp]
theorem submonoid.coe_mul {M : Type u_1} [mul_one_class M] (S : submonoid M) (x y : S) :
x * y = (x) * y
@[simp]
theorem add_submonoid.coe_add {M : Type u_1} [add_zero_class M] (S : add_submonoid M) (x y : S) :
(x + y) = x + y
@[simp]
theorem add_submonoid.coe_zero {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :
0 = 0
@[simp]
theorem submonoid.coe_one {M : Type u_1} [mul_one_class M] (S : submonoid M) :
1 = 1
@[instance]

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

@[instance]

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

Equations
@[instance]
def submonoid.to_monoid {M : Type u_1} [monoid M] (S : submonoid M) :

A submonoid of a monoid inherits a monoid structure.

Equations
@[instance]

An add_submonoid of an add_monoid inherits an add_monoid structure.

@[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
def add_submonoid.subtype {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

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

def submonoid.subtype {M : Type u_1} [mul_one_class M] (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} [add_zero_class M] (S : add_submonoid M) :
@[simp]
theorem submonoid.coe_subtype {M : Type u_1} [mul_one_class M] (S : submonoid M) :
theorem add_submonoid.closure_induction' {M : Type u_1} [add_zero_class M] (s : set M) {p : (add_submonoid.closure s) → Prop} (Hs : ∀ (x : M) (h : x s), p x, _⟩) (H1 : p 0) (Hmul : ∀ (x y : (add_submonoid.closure s)), p xp yp (x + y)) (x : (add_submonoid.closure s)) :
p x

An induction principle on elements of the type add_submonoid.closure s. If p holds for 0 and all elements of s, and is preserved under addition, then p holds for all elements of the closure of s.

The difference with add_submonoid.closure_induction is that this acts on the subtype.

theorem submonoid.closure_induction' {M : Type u_1} [mul_one_class M] (s : set M) {p : (submonoid.closure s) → Prop} (Hs : ∀ (x : M) (h : x s), p x, _⟩) (H1 : p 1) (Hmul : ∀ (x y : (submonoid.closure s)), p xp yp (x * y)) (x : (submonoid.closure s)) :
p x

An induction principle on elements of the type submonoid.closure s. If p holds for 1 and all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

The difference with submonoid.closure_induction is that this acts on the subtype.

def submonoid.prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class 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
def add_submonoid.prod {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :

Given add_submonoids s, t of add_monoids A, B respectively, s × t as an add_submonoid of A × B.

theorem add_submonoid.coe_prod {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :
(s.prod t) = s.prod t
theorem submonoid.coe_prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) (t : submonoid N) :
(s.prod t) = s.prod t
theorem submonoid.mem_prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {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} [add_zero_class M] [add_zero_class N] {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} [add_zero_class M] [add_zero_class N] {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} [mul_one_class M] [mul_one_class N] {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} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) :
theorem submonoid.prod_top {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) :
theorem submonoid.top_prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid N) :
theorem add_submonoid.top_prod {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid N) :
@[simp]
theorem add_submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
@[simp]
theorem submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
theorem add_submonoid.bot_sum_bot {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
theorem submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
def submonoid.prod_equiv {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (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} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :

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

theorem add_submonoid.map_inl {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) :
theorem submonoid.map_inl {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) :
theorem submonoid.map_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid N) :
theorem add_submonoid.map_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid N) :
@[simp]
theorem submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) (t : submonoid N) :
@[simp]
theorem add_submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :
def monoid_hom.mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :

The range of a monoid homomorphism is a submonoid.

Equations
def add_monoid_hom.mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :

The range of an add_monoid_hom is an add_submonoid.

@[simp]
theorem monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :

Note that monoid_hom.mrange is deliberately defined in a way that makes this true by rfl, as this means the types ↥(set.range f) and ↥f.mrange are interchangeable without proof obligations.

@[simp]
theorem add_monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :

Note that add_monoid_hom.mrange is deliberately defined in a way that makes this true by rfl, as this means the types ↥(set.range f) and ↥f.mrange are interchangeable without proof obligations.

@[simp]
theorem add_monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {f : M →+ N} {y : N} :
y f.mrange ∃ (x : M), f x = y
@[simp]
theorem monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f : M →* N} {y : N} :
y f.mrange ∃ (x : M), f x = y
theorem monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :
theorem add_monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
theorem add_monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (g : N →+ P) (f : M →+ N) :
theorem monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (g : N →* P) (f : M →* N) :
theorem monoid_hom.mrange_top_iff_surjective {M : Type u_1} [mul_one_class M] {N : Type u_2} [mul_one_class N] {f : M →* N} :
theorem add_monoid_hom.mrange_top_of_surjective {M : Type u_1} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) (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} [mul_one_class M] {N : Type u_2} [mul_one_class N] (f : M →* N) (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} [mul_one_class M] [mul_one_class N] (f : M →* N) (s : set N) :
theorem add_monoid_hom.map_mclosure {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (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} [mul_one_class M] [mul_one_class N] (f : M →* N) (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 monoid_hom.mrestrict {M : Type u_1} [mul_one_class M] {N : Type u_2} [mul_one_class N] (f : M →* N) (S : submonoid M) :

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

Equations
def add_monoid_hom.mrestrict {M : Type u_1} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) (S : add_submonoid M) :

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

@[simp]
theorem add_monoid_hom.mrestrict_apply {M : Type u_1} [add_zero_class M] (S : add_submonoid M) {N : Type u_2} [add_zero_class N] (f : M →+ N) (x : S) :
(f.mrestrict S) x = f x
@[simp]
theorem monoid_hom.mrestrict_apply {M : Type u_1} [mul_one_class M] (S : submonoid M) {N : Type u_2} [mul_one_class N] (f : M →* N) (x : S) :
(f.mrestrict S) x = f x
def add_monoid_hom.cod_mrestrict {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (S : add_submonoid N) (h : ∀ (x : M), f x S) :

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

def monoid_hom.cod_mrestrict {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (S : submonoid N) (h : ∀ (x : M), f x S) :

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

Equations
def add_monoid_hom.mrange_restrict {M : Type u_1} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) :

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

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

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} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) (x : M) :
@[simp]
theorem monoid_hom.coe_mrange_restrict {M : Type u_1} [mul_one_class M] {N : Type u_2} [mul_one_class N] (f : M →* N) (x : M) :
theorem submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
theorem add_submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
theorem submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
theorem add_submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
theorem submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
theorem submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
@[simp]
theorem submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
@[simp]
theorem add_submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
@[simp]
theorem submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
@[simp]
theorem add_submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
@[simp]
theorem submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
def submonoid.inclusion {M : Type u_1} [mul_one_class M] {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} [add_zero_class M] {S T : add_submonoid M} (h : S T) :

The add_monoid hom associated to an inclusion of submonoids.

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

A submonoid is either the trivial submonoid or nontrivial.

theorem submonoid.bot_or_exists_ne_one {M : Type u_1} [mul_one_class M] (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} [add_zero_class M] (S : add_submonoid M) :
S = ∃ (x : M) (H : x S), x 0
def mul_equiv.submonoid_congr {M : Type u_1} [mul_one_class M] {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} [add_zero_class M] {S T : add_submonoid M} (h : S = T) :

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