mathlib documentation

group_theory.submonoid.basic

Submonoids: definition and complete_lattice structure #

This file defines bundled multiplicative and additive submonoids. We also define a complete_lattice structure on submonoids, 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_mdense.

Main definitions #

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

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 : out_param (Type u_5)) [has_one M] [set_like S M] :
Type
  • 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
@[class]
structure zero_mem_class (S : Type u_4) (M : out_param (Type u_5)) [has_zero M] [set_like S M] :
Type
  • 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
@[class]
structure mul_mem_class (S : Type u_4) (M : out_param (Type u_5)) [has_mul M] [set_like S M] :
Type
  • mul_mem : ∀ {s : S} {a b : M}, a sb sa * b s

mul_mem_class S M says S is a type of subsets s ≤ M that are closed under (*)

Instances
@[class]
structure add_mem_class (S : Type u_4) (M : out_param (Type u_5)) [has_add M] [set_like S M] :
Type
  • add_mem : ∀ {s : S} {a b : M}, a sb sa + b s

add_mem_class S M says S is a type of subsets s ≤ M that are closed under (+)

Instances
structure submonoid (M : Type u_4) [mul_one_class M] :
Type u_4

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

def submonoid.to_subsemigroup {M : Type u_4} [mul_one_class M] (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 : out_param (Type u_5)) [mul_one_class M] [set_like S M] :
Type

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

Instances

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) [add_zero_class M] :
Type u_4

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

@[class]
structure add_submonoid_class (S : Type u_4) (M : out_param (Type u_5)) [add_zero_class M] [set_like S M] :
Type

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

Instances
@[protected, instance]
def add_submonoid_class.to_zero_mem_class (S : Type u_1) (M : out_param (Type u_2)) [add_zero_class M] [set_like S M] [h : add_submonoid_class S M] :
Equations
@[protected, instance]
def submonoid_class.to_one_mem_class (S : Type u_1) (M : out_param (Type u_2)) [mul_one_class M] [set_like S M] [h : submonoid_class S M] :
Equations
theorem pow_mem {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A 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} [set_like A M] [add_submonoid_class A M] {S : A} {x : M} (hx : x S) (n : ) :
n x S
@[protected, instance]
Equations
@[protected, instance]
def submonoid.set_like {M : Type u_1} [mul_one_class M] :
Equations
@[protected, instance]
Equations
@[simp]
theorem add_submonoid.mem_carrier {M : Type u_1} [add_zero_class M] {s : add_submonoid M} {x : M} :
x s.carrier x s
@[simp]
theorem submonoid.mem_carrier {M : Type u_1} [mul_one_class M] {s : submonoid M} {x : M} :
x s.carrier x s
@[simp]
theorem add_submonoid.mem_mk {M : Type u_1} [add_zero_class M] {s : set M} {x : M} (h_one : ∀ {a b : M}, a sb sa + 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} [mul_one_class M] {s : set M} {x : M} (h_one : ∀ {a b : M}, a sb sa * 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} [add_zero_class M] {s : set M} (h_one : ∀ {a b : M}, a sb sa + 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} [mul_one_class M] {s : set M} (h_one : ∀ {a b : M}, a sb sa * 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} [mul_one_class M] {s t : set M} (h_one : ∀ {a b : M}, a sb sa * b s) (h_mul : 1 s) (h_one' : ∀ {a b : M}, a tb ta * 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} [add_zero_class M] {s t : set M} (h_one : ∀ {a b : M}, a sb sa + b s) (h_mul : 0 s) (h_one' : ∀ {a b : M}, a tb ta + 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
theorem add_submonoid.ext {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} (h : ∀ (x : M), x S x T) :
S = T

Two add_submonoids are equal if they have the same elements.

@[ext]
theorem submonoid.ext {M : Type u_1} [mul_one_class M] {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} [mul_one_class M] (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} [add_zero_class M] (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} [add_zero_class M] {S : add_submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
@[simp]
theorem submonoid.coe_copy {M : Type u_1} [mul_one_class M] {S : submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
theorem submonoid.copy_eq {M : Type u_1} [mul_one_class M] {S : submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S
theorem add_submonoid.copy_eq {M : Type u_1} [add_zero_class M] {S : add_submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S
@[protected]
theorem submonoid.one_mem {M : Type u_1} [mul_one_class M] (S : submonoid M) :
1 S

A submonoid contains the monoid's 1.

@[protected]
theorem add_submonoid.zero_mem {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :
0 S

An add_submonoid contains the monoid's 0.

@[protected]
theorem add_submonoid.add_mem {M : Type u_1} [add_zero_class M] (S : add_submonoid M) {x y : M} :
x Sy Sx + y S

An add_submonoid is closed under addition.

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

A submonoid is closed under multiplication.

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

The submonoid M of the monoid M.

Equations
@[protected, instance]

The additive submonoid M of the add_monoid M.

Equations
@[protected, instance]

The trivial add_submonoid {0} of an add_monoid M.

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

The trivial submonoid {1} of an monoid M.

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

The inf of two add_submonoids is their intersection.

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

The inf of two submonoids is their intersection.

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

Submonoids of a monoid form a complete lattice.

Equations
@[protected, instance]

The add_submonoids of an add_monoid form a complete lattice.

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

The submonoid generated by a set.

Equations
def add_submonoid.closure {M : Type u_1} [add_zero_class M] (s : set M) :

The add_submonoid generated by a set

Equations
theorem add_submonoid.mem_closure {M : Type u_1} [add_zero_class M] {s : set M} {x : M} :
x add_submonoid.closure s ∀ (S : add_submonoid M), s Sx S
theorem submonoid.mem_closure {M : Type u_1} [mul_one_class M] {s : set M} {x : M} :
x submonoid.closure s ∀ (S : submonoid M), s Sx S
@[simp]
theorem submonoid.subset_closure {M : Type u_1} [mul_one_class M] {s : set M} :

The submonoid generated by a set includes the set.

@[simp]
theorem add_submonoid.subset_closure {M : Type u_1} [add_zero_class M] {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} [mul_one_class M] {s : set M} {P : M} (hP : P submonoid.closure s) :
P s
theorem add_submonoid.not_mem_of_not_mem_closure {M : Type u_1} [add_zero_class M] {s : set M} {P : M} (hP : P add_submonoid.closure s) :
P s
@[simp]
theorem submonoid.closure_le {M : Type u_1} [mul_one_class M] {s : set M} {S : submonoid M} :

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

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

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

theorem add_submonoid.closure_mono {M : Type u_1} [add_zero_class M] ⦃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} [mul_one_class M] ⦃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} [add_zero_class M] {s : set M} {S : add_submonoid M} (h₁ : s S) (h₂ : S add_submonoid.closure s) :
theorem submonoid.closure_eq_of_le {M : Type u_1} [mul_one_class M] {s : set M} {S : submonoid M} (h₁ : s S) (h₂ : S submonoid.closure s) :
theorem submonoid.closure_induction {M : Type u_1} [mul_one_class M] {s : set M} {p : M → Prop} {x : M} (h : x submonoid.closure s) (Hs : ∀ (x : M), x sp x) (H1 : p 1) (Hmul : ∀ (x y : M), p xp yp (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} [add_zero_class M] {s : set M} {p : M → Prop} {x : M} (h : x add_submonoid.closure s) (Hs : ∀ (x : M), x sp x) (H1 : p 0) (Hmul : ∀ (x y : M), p xp yp (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} [add_zero_class M] (s : set M) {p : Π (x : M), x add_submonoid.closure s → Prop} (Hs : ∀ (x : M) (h : x s), p x _) (H1 : p 0 _) (Hmul : ∀ (x : M) (hx : x add_submonoid.closure s) (y : M) (hy : y add_submonoid.closure s), p x hxp y hyp (x + y) _) {x : M} (hx : x add_submonoid.closure s) :
p x hx

A dependent version of add_submonoid.closure_induction.

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

A dependent version of submonoid.closure_induction.

theorem add_submonoid.closure_induction₂ {M : Type u_1} [add_zero_class M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x add_submonoid.closure s) (hy : y add_submonoid.closure s) (Hs : ∀ (x : M), x s∀ (y : M), y sp x y) (H1_left : ∀ (x : M), p 0 x) (H1_right : ∀ (x : M), p x 0) (Hmul_left : ∀ (x y z : M), p x zp y zp (x + y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp 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} [mul_one_class M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x submonoid.closure s) (hy : y submonoid.closure s) (Hs : ∀ (x : M), x s∀ (y : M), y sp x y) (H1_left : ∀ (x : M), p 1 x) (H1_right : ∀ (x : M), p x 1) (Hmul_left : ∀ (x y z : M), p x zp y zp (x * y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp 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} [add_zero_class M] {p : M → Prop} (x : M) {s : set M} (hs : add_submonoid.closure s = ) (Hs : ∀ (x : M), x sp x) (H1 : p 0) (Hmul : ∀ (x y : M), p xp yp (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} [mul_one_class M] {p : M → Prop} (x : M) {s : set M} (hs : submonoid.closure s = ) (Hs : ∀ (x : M), x sp x) (H1 : p 1) (Hmul : ∀ (x y : M), p xp yp (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]

closure forms a Galois insertion with the coercion to set.

Equations
@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
@[simp]
theorem submonoid.closure_eq {M : Type u_1} [mul_one_class M] (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_Union {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (s : ι → set M) :
add_submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_submonoid.closure (s i)
theorem submonoid.closure_Union {M : Type u_1} [mul_one_class M] {ι : 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} [mul_one_class M] (m : M) (p : submonoid M) :
@[simp]
theorem submonoid.mem_supr {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (p : ι → submonoid M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : submonoid M), (∀ (i : ι), p i N)m N
theorem add_submonoid.mem_supr {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (p : ι → add_submonoid M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : add_submonoid M), (∀ (i : ι), p i N)m N
theorem add_submonoid.supr_eq_closure {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (p : ι → add_submonoid M) :
(⨆ (i : ι), p i) = add_submonoid.closure (⋃ (i : ι), (p i))
theorem submonoid.supr_eq_closure {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (p : ι → submonoid M) :
(⨆ (i : ι), p i) = submonoid.closure (⋃ (i : ι), (p i))
theorem submonoid.disjoint_def {M : Type u_1} [mul_one_class M] {p₁ p₂ : submonoid M} :
disjoint p₁ p₂ ∀ {x : M}, x p₁x p₂x = 1
theorem add_submonoid.disjoint_def {M : Type u_1} [add_zero_class M] {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} [add_zero_class M] {p₁ p₂ : add_submonoid M} :
disjoint p₁ p₂ ∀ {x y : M}, x p₁y p₂x = yx = 0
theorem submonoid.disjoint_def' {M : Type u_1} [mul_one_class M] {p₁ p₂ : submonoid M} :
disjoint p₁ p₂ ∀ {x y : M}, x p₁y p₂x = yx = 1
def add_monoid_hom.eq_mlocus {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (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} [mul_one_class M] [mul_one_class N] (f g : M →* N) :

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

Equations
theorem monoid_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f g : M →* N} {s : set M} (h : set.eq_on f g s) :

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} [add_zero_class M] [add_zero_class N] {f g : M →+ N} {s : set M} (h : set.eq_on f g s) :
theorem monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f g : M →* N} (h : set.eq_on f g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {f g : M →+ N} (h : set.eq_on f g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {s : set M} (hs : add_submonoid.closure s = ) {f g : M →+ N} (h : set.eq_on f g s) :
f = g
theorem monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {s : set M} (hs : submonoid.closure s = ) {f g : M →* N} (h : set.eq_on f g s) :
f = g
def is_add_unit.add_submonoid (M : Type u_1) [add_monoid M] :

The additive submonoid consisting of the additive units of an additive monoid

Equations
def is_unit.submonoid (M : Type u_1) [monoid M] :

The submonoid consisting of the units of a monoid

Equations
theorem is_unit.mem_submonoid_iff {M : Type u_1} [monoid M] (a : M) :
def monoid_hom.of_mdense {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y sf (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_mdense defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s.

Equations
def add_monoid_hom.of_mdense {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (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_mdense defines an additive 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 add_monoid_hom.coe_of_mdense {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
@[simp, norm_cast]
theorem monoid_hom.coe_of_mdense {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y sf (x * y) = (f x) * f y) :
(monoid_hom.of_mdense f hs h1 hmul) = f