mathlib3documentation

group_theory.submonoid.basic

Submonoids: definition and `complete_lattice` structure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines bundled multiplicative and additive submonoids. We also define a `complete_lattice` structure on `submonoid`s, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with `closure s = ⊤`) to the whole monoid, see `submonoid.dense_induction` and `monoid_hom.of_mclosure_eq_top_left`/`monoid_hom.of_mclosure_eq_top_right`.

Main definitions #

• `submonoid M`: the type of bundled submonoids of a monoid `M`; the underlying set is given in the `carrier` field of the structure, and should be accessed through coercion as in `(S : set M)`.
• `add_submonoid M` : the type of bundled submonoids of an additive monoid `M`.

For each of the following definitions in the `submonoid` namespace, there is a corresponding definition in the `add_submonoid` namespace.

• `submonoid.copy` : copy of a submonoid with `carrier` replaced by a set that is equal but possibly not definitionally equal to the carrier of the original `submonoid`.
• `submonoid.closure` : monoid closure of a set, i.e., the least submonoid that includes the set.
• `submonoid.gi` : `closure : set M → submonoid M` and coercion `coe : submonoid M → set M` form a `galois_insertion`;
• `monoid_hom.eq_mlocus`: the submonoid of elements `x : M` such that `f x = g x`;
• `monoid_hom.of_mclosure_eq_top_right`: if a map `f : M → N` between two monoids satisfies `f 1 = 1` and `f (x * y) = f x * f y` for `y` from some dense set `s`, then `f` is a monoid homomorphism. E.g., if `f : ℕ → M` satisfies `f 0 = 0` and `f (x + 1) = f x + f 1`, then `f` is an additive monoid homomorphism.

Implementation notes #

Submonoid inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as membership of a submonoid's underlying set.

Note that `submonoid M` does not actually require `monoid M`, instead requiring only the weaker `mul_one_class M`.

This file is designed to have very few dependencies. In particular, it should not use natural numbers. `submonoid` is implemented by extending `subsemigroup` requiring `one_mem'`.

Tags #

submonoid, submonoids

@[class]
structure one_mem_class (S : Type u_4) (M : Type u_5) [has_one M] [ M] :
Prop
• one_mem : (s : S), 1 s

`one_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`.

Instances of this typeclass
@[class]
structure zero_mem_class (S : Type u_4) (M : Type u_5) [has_zero M] [ M] :
Prop
• zero_mem : (s : S), 0 s

`zero_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`.

Instances of this typeclass
structure submonoid (M : Type u_4)  :
Type u_4

A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication.

Instances for `submonoid`
def submonoid.to_subsemigroup {M : Type u_4} (self : submonoid M) :

A submonoid of a monoid `M` can be considered as a subsemigroup of that monoid.

@[class]
structure submonoid_class (S : Type u_4) (M : Type u_5) [ M] :
Prop
• to_mul_mem_class :
• to_one_mem_class :

`submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `1` and are closed under `(*)`

Instances of this typeclass

An additive submonoid of an additive monoid `M` can be considered as an additive subsemigroup of that additive monoid.

structure add_submonoid (M : Type u_4)  :
Type u_4

An additive submonoid of an additive monoid `M` is a subset containing 0 and closed under addition.

Instances for `add_submonoid`
@[class]
structure add_submonoid_class (S : Type u_4) (M : Type u_5) [ M] :
Prop
• to_zero_mem_class :

`add_submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `0` and are closed under `(+)`

Instances of this typeclass
theorem pow_mem {M : Type u_1} [monoid M] {A : Type u_2} [ M] [ M] {S : A} {x : M} (hx : x S) (n : ) :
x ^ n S
theorem nsmul_mem {M : Type u_1} [add_monoid M] {A : Type u_2} [ M] [ M] {S : A} {x : M} (hx : x S) (n : ) :
n x S
@[protected, instance]
def add_submonoid.set_like {M : Type u_1}  :
M
Equations
@[protected, instance]
def submonoid.set_like {M : Type u_1}  :
M
Equations
@[protected, instance]
@[protected, instance]
def submonoid.submonoid_class {M : Type u_1}  :
M
set M
Equations
def submonoid.simps.coe {M : Type u_1} (S : submonoid M) :
set M
Equations
@[simp]
theorem add_submonoid.mem_carrier {M : Type u_1} {s : add_submonoid M} {x : M} :
x s.carrier x s
@[simp]
theorem submonoid.mem_carrier {M : Type u_1} {s : submonoid M} {x : M} :
x s.carrier x s
@[simp]
theorem add_submonoid.mem_mk {M : Type u_1} {s : set M} {x : M} (h_one : {a b : M}, a s b s a + b s) (h_mul : 0 s) :
x {carrier := s, add_mem' := h_one, zero_mem' := h_mul} x s
@[simp]
theorem submonoid.mem_mk {M : Type u_1} {s : set M} {x : M} (h_one : {a b : M}, a s b s a * b s) (h_mul : 1 s) :
x {carrier := s, mul_mem' := h_one, one_mem' := h_mul} x s
@[simp]
theorem add_submonoid.coe_set_mk {M : Type u_1} {s : set M} (h_one : {a b : M}, a s b s a + b s) (h_mul : 0 s) :
{carrier := s, add_mem' := h_one, zero_mem' := h_mul} = s
@[simp]
theorem submonoid.coe_set_mk {M : Type u_1} {s : set M} (h_one : {a b : M}, a s b s a * b s) (h_mul : 1 s) :
{carrier := s, mul_mem' := h_one, one_mem' := h_mul} = s
@[simp]
theorem submonoid.mk_le_mk {M : Type u_1} {s t : set M} (h_one : {a b : M}, a s b s a * b s) (h_mul : 1 s) (h_one' : {a b : M}, a t b t a * b t) (h_mul' : 1 t) :
{carrier := s, mul_mem' := h_one, one_mem' := h_mul} {carrier := t, mul_mem' := h_one', one_mem' := h_mul'} s t
@[simp]
theorem add_submonoid.mk_le_mk {M : Type u_1} {s t : set M} (h_one : {a b : M}, a s b s a + b s) (h_mul : 0 s) (h_one' : {a b : M}, a t b t a + b t) (h_mul' : 0 t) :
{carrier := s, add_mem' := h_one, zero_mem' := h_mul} {carrier := t, add_mem' := h_one', zero_mem' := h_mul'} s t
@[ext]
theorem add_submonoid.ext {M : Type u_1} {S T : add_submonoid M} (h : (x : M), x S x T) :
S = T

Two `add_submonoid`s are equal if they have the same elements.

@[ext]
theorem submonoid.ext {M : Type u_1} {S T : submonoid M} (h : (x : M), x S x T) :
S = T

Two submonoids are equal if they have the same elements.

@[protected]
def submonoid.copy {M : Type u_1} (S : submonoid M) (s : set M) (hs : s = S) :

Copy a submonoid replacing `carrier` with a set that is equal to it.

Equations
@[protected]
def add_submonoid.copy {M : Type u_1} (S : add_submonoid M) (s : set M) (hs : s = S) :

Copy an additive submonoid replacing `carrier` with a set that is equal to it.

Equations
@[simp]
theorem add_submonoid.coe_copy {M : Type u_1} {S : add_submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
@[simp]
theorem submonoid.coe_copy {M : Type u_1} {S : submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
theorem submonoid.copy_eq {M : Type u_1} {S : submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S
theorem add_submonoid.copy_eq {M : Type u_1} {S : add_submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S
@[protected]
theorem submonoid.one_mem {M : Type u_1} (S : submonoid M) :
1 S

A submonoid contains the monoid's 1.

@[protected]
0 S

An `add_submonoid` contains the monoid's 0.

@[protected]
x S y S x + y S

An `add_submonoid` is closed under addition.

@[protected]
theorem submonoid.mul_mem {M : Type u_1} (S : submonoid M) {x y : M} :
x S y S x * y S

A submonoid is closed under multiplication.

@[protected, instance]
def submonoid.has_top {M : Type u_1}  :

The submonoid `M` of the monoid `M`.

Equations
@[protected, instance]
def add_submonoid.has_top {M : Type u_1}  :

The additive submonoid `M` of the `add_monoid M`.

Equations
@[protected, instance]
def add_submonoid.has_bot {M : Type u_1}  :

The trivial `add_submonoid` `{0}` of an `add_monoid` `M`.

Equations
@[protected, instance]
def submonoid.has_bot {M : Type u_1}  :

The trivial submonoid `{1}` of an monoid `M`.

Equations
@[protected, instance]
def add_submonoid.inhabited {M : Type u_1}  :
Equations
@[protected, instance]
def submonoid.inhabited {M : Type u_1}  :
Equations
@[simp]
theorem submonoid.mem_bot {M : Type u_1} {x : M} :
x x = 1
@[simp]
theorem add_submonoid.mem_bot {M : Type u_1} {x : M} :
x x = 0
@[simp]
theorem submonoid.mem_top {M : Type u_1} (x : M) :
@[simp]
theorem add_submonoid.mem_top {M : Type u_1} (x : M) :
@[simp]
theorem add_submonoid.coe_top {M : Type u_1}  :
@[simp]
theorem submonoid.coe_top {M : Type u_1}  :
@[simp]
theorem submonoid.coe_bot {M : Type u_1}  :
= {1}
@[simp]
theorem add_submonoid.coe_bot {M : Type u_1}  :
= {0}
@[protected, instance]
def add_submonoid.has_inf {M : Type u_1}  :

The inf of two `add_submonoid`s is their intersection.

Equations
@[protected, instance]
def submonoid.has_inf {M : Type u_1}  :

The inf of two submonoids is their intersection.

Equations
@[simp]
theorem add_submonoid.coe_inf {M : Type u_1} (p p' : add_submonoid M) :
(p p') = p p'
@[simp]
theorem submonoid.coe_inf {M : Type u_1} (p p' : submonoid M) :
(p p') = p p'
@[simp]
theorem add_submonoid.mem_inf {M : Type u_1} {p p' : add_submonoid M} {x : M} :
x p p' x p x p'
@[simp]
theorem submonoid.mem_inf {M : Type u_1} {p p' : submonoid M} {x : M} :
x p p' x p x p'
@[protected, instance]
def submonoid.has_Inf {M : Type u_1}  :
Equations
@[protected, instance]
def add_submonoid.has_Inf {M : Type u_1}  :
Equations
@[simp, norm_cast]
theorem submonoid.coe_Inf {M : Type u_1} (S : set (submonoid M)) :
(has_Inf.Inf S) = (s : (H : s S), s
@[simp, norm_cast]
theorem add_submonoid.coe_Inf {M : Type u_1} (S : set ) :
(has_Inf.Inf S) = (s : (H : s S), s
theorem add_submonoid.mem_Inf {M : Type u_1} {S : set } {x : M} :
x (p : , p S x p
theorem submonoid.mem_Inf {M : Type u_1} {S : set (submonoid M)} {x : M} :
x (p : , p S x p
theorem submonoid.mem_infi {M : Type u_1} {ι : Sort u_2} {S : ι } {x : M} :
(x (i : ι), S i) (i : ι), x S i
theorem add_submonoid.mem_infi {M : Type u_1} {ι : Sort u_2} {S : ι } {x : M} :
(x (i : ι), S i) (i : ι), x S i
@[simp, norm_cast]
theorem submonoid.coe_infi {M : Type u_1} {ι : Sort u_2} {S : ι } :
( (i : ι), S i) = (i : ι), (S i)
@[simp, norm_cast]
theorem add_submonoid.coe_infi {M : Type u_1} {ι : Sort u_2} {S : ι } :
( (i : ι), S i) = (i : ι), (S i)
@[protected, instance]
def submonoid.complete_lattice {M : Type u_1}  :

Submonoids of a monoid form a complete lattice.

Equations
@[protected, instance]

The `add_submonoid`s of an `add_monoid` form a complete lattice.

Equations
@[simp]
theorem add_submonoid.subsingleton_iff {M : Type u_1}  :
@[simp]
theorem submonoid.subsingleton_iff {M : Type u_1}  :
@[simp]
theorem add_submonoid.nontrivial_iff {M : Type u_1}  :
@[simp]
theorem submonoid.nontrivial_iff {M : Type u_1}  :
@[protected, instance]
def add_submonoid.unique {M : Type u_1} [subsingleton M] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def submonoid.nontrivial {M : Type u_1} [nontrivial M] :
@[protected, instance]
def submonoid.closure {M : Type u_1} (s : set M) :

The `submonoid` generated by a set.

Equations
Instances for `↥submonoid.closure`
def add_submonoid.closure {M : Type u_1} (s : set M) :

The `add_submonoid` generated by a set

Equations
Instances for `↥add_submonoid.closure`
theorem add_submonoid.mem_closure {M : Type u_1} {s : set M} {x : M} :
(S : , s S x S
theorem submonoid.mem_closure {M : Type u_1} {s : set M} {x : M} :
(S : , s S x S
@[simp]
theorem submonoid.subset_closure {M : Type u_1} {s : set M} :
s

The submonoid generated by a set includes the set.

@[simp]
theorem add_submonoid.subset_closure {M : Type u_1} {s : set M} :

The `add_submonoid` generated by a set includes the set.

theorem submonoid.not_mem_of_not_mem_closure {M : Type u_1} {s : set M} {P : M} (hP : P ) :
P s
theorem add_submonoid.not_mem_of_not_mem_closure {M : Type u_1} {s : set M} {P : M} (hP : P ) :
P s
@[simp]
theorem submonoid.closure_le {M : Type u_1} {s : set M} {S : submonoid M} :
s S

A submonoid `S` includes `closure s` if and only if it includes `s`.

@[simp]
theorem add_submonoid.closure_le {M : Type u_1} {s : set M} {S : add_submonoid M} :
s S

An additive submonoid `S` includes `closure s` if and only if it includes `s`

theorem add_submonoid.closure_mono {M : Type u_1} ⦃s t : set M⦄ (h : s t) :

Additive submonoid closure of a set is monotone in its argument: if `s ⊆ t`, then `closure s ≤ closure t`

theorem submonoid.closure_mono {M : Type u_1} ⦃s t : set M⦄ (h : s t) :

Submonoid closure of a set is monotone in its argument: if `s ⊆ t`, then `closure s ≤ closure t`.

theorem add_submonoid.closure_eq_of_le {M : Type u_1} {s : set M} {S : add_submonoid M} (h₁ : s S) (h₂ : S ) :
theorem submonoid.closure_eq_of_le {M : Type u_1} {s : set M} {S : submonoid M} (h₁ : s S) (h₂ : S ) :
theorem submonoid.closure_induction {M : Type u_1} {s : set M} {p : M Prop} {x : M} (h : x ) (Hs : (x : M), x s p x) (H1 : p 1) (Hmul : (x y : M), p x p y p (x * y)) :
p x

An induction principle for closure membership. 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`.

theorem add_submonoid.closure_induction {M : Type u_1} {s : set M} {p : M Prop} {x : M} (h : x ) (Hs : (x : M), x s p x) (H1 : p 0) (Hmul : (x y : M), p x p y p (x + y)) :
p x

An induction principle for additive closure membership. If `p` holds for `0` and all elements of `s`, and is preserved under addition, then `p` holds for all elements of the additive closure of `s`.

theorem add_submonoid.closure_induction' {M : Type u_1} (s : set M) {p : Π (x : M), Prop} (Hs : (x : M) (h : x s), p x _) (H1 : p 0 _) (Hmul : (x : M) (hx : (y : M) (hy : , p x hx p y hy p (x + y) _) {x : M} (hx : x ) :
p x hx

A dependent version of `add_submonoid.closure_induction`.

theorem submonoid.closure_induction' {M : Type u_1} (s : set M) {p : Π (x : M), Prop} (Hs : (x : M) (h : x s), p x _) (H1 : p 1 _) (Hmul : (x : M) (hx : (y : M) (hy : , p x hx p y hy p (x * y) _) {x : M} (hx : x ) :
p x hx

A dependent version of `submonoid.closure_induction`.

theorem add_submonoid.closure_induction₂ {M : Type u_1} {s : set M} {p : M M Prop} {x y : M} (hx : x ) (hy : y ) (Hs : (x : M), x s (y : M), y s p x y) (H1_left : (x : M), p 0 x) (H1_right : (x : M), p x 0) (Hmul_left : (x y z : M), p x z p y z p (x + y) z) (Hmul_right : (x y z : M), p z x p z y p z (x + y)) :
p x y

An induction principle for additive closure membership for predicates with two arguments.

theorem submonoid.closure_induction₂ {M : Type u_1} {s : set M} {p : M M Prop} {x y : M} (hx : x ) (hy : y ) (Hs : (x : M), x s (y : M), y s p x y) (H1_left : (x : M), p 1 x) (H1_right : (x : M), p x 1) (Hmul_left : (x y z : M), p x z p y z p (x * y) z) (Hmul_right : (x y z : M), p z x p z y p z (x * y)) :
p x y

An induction principle for closure membership for predicates with two arguments.

theorem add_submonoid.dense_induction {M : Type u_1} {p : M Prop} (x : M) {s : set M} (hs : = ) (Hs : (x : M), x s p x) (H1 : p 0) (Hmul : (x y : M), p x p y p (x + y)) :
p x

If `s` is a dense set in an additive monoid `M`, `add_submonoid.closure s = ⊤`, then in order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`, verify `p 0`, and verify that `p x` and `p y` imply `p (x + y)`.

theorem submonoid.dense_induction {M : Type u_1} {p : M Prop} (x : M) {s : set M} (hs : = ) (Hs : (x : M), x s p x) (H1 : p 1) (Hmul : (x y : M), p x p y p (x * y)) :
p x

If `s` is a dense set in a monoid `M`, `submonoid.closure s = ⊤`, then in order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`, verify `p 1`, and verify that `p x` and `p y` imply `p (x * y)`.

@[protected]
def add_submonoid.gi (M : Type u_1)  :

`closure` forms a Galois insertion with the coercion to set.

Equations
@[protected]
def submonoid.gi (M : Type u_1)  :

`closure` forms a Galois insertion with the coercion to set.

Equations
@[simp]
theorem submonoid.closure_eq {M : Type u_1} (S : submonoid M) :

Closure of a submonoid `S` equals `S`.

@[simp]

Additive closure of an additive submonoid `S` equals `S`

@[simp]
theorem add_submonoid.closure_empty {M : Type u_1}  :
@[simp]
theorem submonoid.closure_empty {M : Type u_1}  :
@[simp]
theorem add_submonoid.closure_univ {M : Type u_1}  :
@[simp]
theorem submonoid.closure_univ {M : Type u_1}  :
theorem submonoid.closure_union {M : Type u_1} (s t : set M) :
theorem add_submonoid.closure_union {M : Type u_1} (s t : set M) :
theorem add_submonoid.closure_Union {M : Type u_1} {ι : Sort u_2} (s : ι set M) :
add_submonoid.closure ( (i : ι), s i) = (i : ι),
theorem submonoid.closure_Union {M : Type u_1} {ι : Sort u_2} (s : ι set M) :
submonoid.closure ( (i : ι), s i) = (i : ι), submonoid.closure (s i)
@[simp]
theorem submonoid.closure_singleton_le_iff_mem {M : Type u_1} (m : M) (p : submonoid M) :
p m p
@[simp]
theorem add_submonoid.closure_singleton_le_iff_mem {M : Type u_1} (m : M) (p : add_submonoid M) :
m p
theorem submonoid.mem_supr {M : Type u_1} {ι : Sort u_2} (p : ι ) {m : M} :
(m (i : ι), p i) (N : , ( (i : ι), p i N) m N
theorem add_submonoid.mem_supr {M : Type u_1} {ι : Sort u_2} (p : ι ) {m : M} :
(m (i : ι), p i) (N : , ( (i : ι), p i N) m N
theorem add_submonoid.supr_eq_closure {M : Type u_1} {ι : Sort u_2} (p : ι ) :
( (i : ι), p i) = add_submonoid.closure ( (i : ι), (p i))
theorem submonoid.supr_eq_closure {M : Type u_1} {ι : Sort u_2} (p : ι ) :
( (i : ι), p i) = submonoid.closure ( (i : ι), (p i))
theorem submonoid.disjoint_def {M : Type u_1} {p₁ p₂ : submonoid M} :
disjoint p₁ p₂ {x : M}, x p₁ x p₂ x = 1
theorem add_submonoid.disjoint_def {M : Type u_1} {p₁ p₂ : add_submonoid M} :
disjoint p₁ p₂ {x : M}, x p₁ x p₂ x = 0
theorem add_submonoid.disjoint_def' {M : Type u_1} {p₁ p₂ : add_submonoid M} :
disjoint p₁ p₂ {x y : M}, x p₁ y p₂ x = y x = 0
theorem submonoid.disjoint_def' {M : Type u_1} {p₁ p₂ : submonoid M} :
disjoint p₁ p₂ {x y : M}, x p₁ y p₂ x = y x = 1
def add_monoid_hom.eq_mlocus {M : Type u_1} {N : Type u_2} (f g : M →+ N) :

The additive submonoid of elements `x : M` such that `f x = g x`

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

The submonoid of elements `x : M` such that `f x = g x`

Equations
@[simp]
theorem add_monoid_hom.eq_mlocus_same {M : Type u_1} {N : Type u_2} (f : M →+ N) :
@[simp]
theorem monoid_hom.eq_mlocus_same {M : Type u_1} {N : Type u_2} (f : M →* N) :
theorem monoid_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} {f g : M →* N} {s : set M} (h : g s) :
g

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem add_monoid_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} {f g : M →+ N} {s : set M} (h : g s) :

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} {f g : M →* N} (h : g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} {f g : M →+ N} (h : g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} {s : set M} (hs : = ) {f g : M →+ N} (h : g s) :
f = g
theorem monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} {s : set M} (hs : = ) {f g : M →* N} (h : g s) :
f = g

Equations
Instances for `↥is_add_unit.add_submonoid`
def is_unit.submonoid (M : Type u_1) [monoid M] :

The submonoid consisting of the units of a monoid

Equations
Instances for `↥is_unit.submonoid`
theorem is_unit.mem_submonoid_iff {M : Type u_1} [monoid M] (a : M) :
def add_monoid_hom.of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 0 = 0) (hmul : (x : M), x s (y : M), f (x + y) = f x + f y) :
M →+ N

/-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is the whole monoid. Then `add_monoid_hom.of_mclosure_eq_top_left` defines an additive monoid homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `x ∈ s`. -/

Equations
def monoid_hom.of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 1 = 1) (hmul : (x : M), x s (y : M), f (x * y) = f x * f y) :
M →* N

Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid. Then `monoid_hom.of_mclosure_eq_top_left` defines a monoid homomorphism from `M` asking for a proof of `f (x * y) = f x * f y` only for `x ∈ s`.

Equations
@[simp, norm_cast]
theorem monoid_hom.coe_of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 1 = 1) (hmul : (x : M), x s (y : M), f (x * y) = f x * f y) :
hmul) = f
@[simp, norm_cast]
theorem add_monoid_hom.coe_of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 0 = 0) (hmul : (x : M), x s (y : M), f (x + y) = f x + f y) :
hmul) = f
def add_monoid_hom.of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 0 = 0) (hmul : (x y : M), y s f (x + y) = f x + f y) :
M →+ N

/-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is the whole monoid. Then `add_monoid_hom.of_mclosure_eq_top_right` defines an additive monoid homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `y ∈ s`. -/

Equations
def monoid_hom.of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 1 = 1) (hmul : (x y : M), y s f (x * y) = f x * f y) :
M →* N

Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid. Then `monoid_hom.of_mclosure_eq_top_right` defines a monoid homomorphism from `M` asking for a proof of `f (x * y) = f x * f y` only for `y ∈ s`.

Equations
@[simp, norm_cast]
theorem monoid_hom.coe_of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 1 = 1) (hmul : (x y : M), y s f (x * y) = f x * f y) :
hmul) = f
@[simp, norm_cast]
theorem add_monoid_hom.coe_of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M N) (hs : = ) (h1 : f 0 = 0) (hmul : (x y : M), y s f (x + y) = f x + f y) :
hmul) = f