mathlib documentation

deprecated.submonoid

Unbundled submonoids #

This file defines unbundled multiplicative and additive submonoids is_submonoid and is_add_submonoid. These are not the preferred way to talk about submonoids and should not be used for any new projects. The preferred way in mathlib are the bundled versions submonoid G and add_submonoid G.

Main definitions #

is_add_submonoid (S : set G) : the predicate that S is the underlying subset of an additive submonoid of G. The bundled variant add_subgroup G should be used in preference to this.

is_submonoid (S : set G) : the predicate that S is the underlying subset of a submonoid of G. The bundled variant submonoid G should be used in preference to this.

Tags #

subgroup, subgroups, is_subgroup

Tags #

submonoid, submonoids, is_submonoid

structure is_add_submonoid {A : Type u_2} [add_monoid A] (s : set A) :
Prop
  • zero_mem : 0 s
  • add_mem : ∀ {a b : A}, a sb sa + b s

s is an additive submonoid: a set containing 0 and closed under addition. Note that this structure is deprecated, and the bundled variant add_submonoid A should be preferred.

structure is_submonoid {M : Type u_1} [monoid M] (s : set M) :
Prop
  • one_mem : 1 s
  • mul_mem : ∀ {a b : M}, a sb sa * b s

s is a submonoid: a set containing 1 and closed under multiplication. Note that this structure is deprecated, and the bundled variant submonoid M should be preferred.

theorem additive.is_add_submonoid {M : Type u_1} [monoid M] {s : set M} (is : is_submonoid s) :
theorem additive.is_add_submonoid_iff {M : Type u_1} [monoid M] {s : set M} :
theorem multiplicative.is_submonoid {A : Type u_2} [add_monoid A] {s : set A} (is : is_add_submonoid s) :
theorem is_add_submonoid.inter {M : Type u_1} [add_monoid M] {s₁ s₂ : set M} (is₁ : is_add_submonoid s₁) (is₂ : is_add_submonoid s₂) :
is_add_submonoid (s₁ s₂)

The intersection of two add_submonoids of an add_monoid M is an add_submonoid of M.

theorem is_submonoid.inter {M : Type u_1} [monoid M] {s₁ s₂ : set M} (is₁ : is_submonoid s₁) (is₂ : is_submonoid s₂) :
is_submonoid (s₁ s₂)

The intersection of two submonoids of a monoid M is a submonoid of M.

theorem is_submonoid.Inter {M : Type u_1} [monoid M] {ι : Sort u_2} {s : ι → set M} (h : ∀ (y : ι), is_submonoid (s y)) :

The intersection of an indexed set of submonoids of a monoid M is a submonoid of M.

theorem is_add_submonoid.Inter {M : Type u_1} [add_monoid M] {ι : Sort u_2} {s : ι → set M} (h : ∀ (y : ι), is_add_submonoid (s y)) :

The intersection of an indexed set of add_submonoids of an add_monoid M is an add_submonoid of M.

theorem is_add_submonoid_Union_of_directed {M : Type u_1} [add_monoid M] {ι : Type u_2} [hι : nonempty ι] {s : ι → set M} (hs : ∀ (i : ι), is_add_submonoid (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_add_submonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of add_submonoids of an add_monoid M is an add_submonoid of M.

theorem is_submonoid_Union_of_directed {M : Type u_1} [monoid M] {ι : Type u_2} [hι : nonempty ι] {s : ι → set M} (hs : ∀ (i : ι), is_submonoid (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_submonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of submonoids of a monoid M is a submonoid of M.

def powers {M : Type u_1} [monoid M] (x : M) :
set M

The set of natural number powers 1, x, x², ... of an element x of a monoid.

Equations
def multiples {A : Type u_2} [add_monoid A] (x : A) :
set A

The set of natural number multiples 0, x, 2x, ... of an element x of an add_monoid.

Equations
theorem powers.one_mem {M : Type u_1} [monoid M] {x : M} :

1 is in the set of natural number powers of an element of a monoid.

theorem multiples.zero_mem {A : Type u_2} [add_monoid A] {x : A} :

0 is in the set of natural number multiples of an element of an add_monoid.

theorem powers.self_mem {M : Type u_1} [monoid M] {x : M} :

An element of a monoid is in the set of that element's natural number powers.

theorem multiples.self_mem {A : Type u_2} [add_monoid A] {x : A} :

An element of an add_monoid is in the set of that element's natural number multiples.

theorem powers.mul_mem {M : Type u_1} [monoid M] {x y z : M} :
y powers xz powers xy * z powers x

The set of natural number powers of an element of a monoid is closed under multiplication.

theorem multiples.add_mem {A : Type u_2} [add_monoid A] {x y z : A} :
y multiples xz multiples xy + z multiples x

The set of natural number multiples of an element of an add_monoid is closed under addition.

theorem multiples.is_add_submonoid {M : Type u_1} [add_monoid M] (x : M) :

The set of natural number multiples of an element of an add_monoid M is an add_submonoid of M.

theorem powers.is_submonoid {M : Type u_1} [monoid M] (x : M) :

The set of natural number powers of an element of a monoid M is a submonoid of M.

theorem univ.is_submonoid {M : Type u_1} [monoid M] :

A monoid is a submonoid of itself.

An add_monoid is an add_submonoid of itself.

theorem is_add_submonoid.preimage {M : Type u_1} [add_monoid M] {N : Type u_2} [add_monoid N] {f : M → N} (hf : is_add_monoid_hom f) {s : set N} (hs : is_add_submonoid s) :

The preimage of an add_submonoid under an add_monoid hom is an add_submonoid of the domain.

theorem is_submonoid.preimage {M : Type u_1} [monoid M] {N : Type u_2} [monoid N] {f : M → N} (hf : is_monoid_hom f) {s : set N} (hs : is_submonoid s) :

The preimage of a submonoid under a monoid hom is a submonoid of the domain.

theorem is_submonoid.image {M : Type u_1} [monoid M] {γ : Type u_2} [monoid γ] {f : M → γ} (hf : is_monoid_hom f) {s : set M} (hs : is_submonoid s) :

The image of a submonoid under a monoid hom is a submonoid of the codomain.

theorem is_add_submonoid.image {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] {f : M → γ} (hf : is_add_monoid_hom f) {s : set M} (hs : is_add_submonoid s) :

The image of an add_submonoid under an add_monoid hom is an add_submonoid of the codomain.

theorem range.is_submonoid {M : Type u_1} [monoid M] {γ : Type u_2} [monoid γ] {f : M → γ} (hf : is_monoid_hom f) :

The image of a monoid hom is a submonoid of the codomain.

theorem range.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] {f : M → γ} (hf : is_add_monoid_hom f) :

The image of an add_monoid hom is an add_submonoid of the codomain.

theorem is_submonoid.pow_mem {M : Type u_1} [monoid M] {s : set M} {a : M} (hs : is_submonoid s) (h : a s) {n : } :
a ^ n s

Submonoids are closed under natural powers.

theorem is_add_submonoid.smul_mem {A : Type u_2} [add_monoid A] {t : set A} {a : A} (ht : is_add_submonoid t) (h : a t) {n : } :
n a t

An add_submonoid is closed under multiplication by naturals.

theorem is_submonoid.power_subset {M : Type u_1} [monoid M] {s : set M} {a : M} (hs : is_submonoid s) (h : a s) :

The set of natural number powers of an element of a submonoid is a subset of the submonoid.

theorem is_add_submonoid.multiple_subset {A : Type u_2} [add_monoid A] {t : set A} {a : A} (ht : is_add_submonoid t) :
a tmultiples a t

The set of natural number multiples of an element of an add_submonoid is a subset of the add_submonoid.

theorem is_add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] {s : set M} (hs : is_add_submonoid s) {l : list M} :
(∀ (x : M), x lx s)l.sum s

The sum of a list of elements of an add_submonoid is an element of the add_submonoid.

theorem is_submonoid.list_prod_mem {M : Type u_1} [monoid M] {s : set M} (hs : is_submonoid s) {l : list M} :
(∀ (x : M), x lx s)l.prod s

The product of a list of elements of a submonoid is an element of the submonoid.

theorem is_submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] {s : set M} (hs : is_submonoid s) (m : multiset M) :
(∀ (a : M), a ma s)m.prod s

The product of a multiset of elements of a submonoid of a comm_monoid is an element of the submonoid.

theorem is_add_submonoid.multiset_sum_mem {M : Type u_1} [add_comm_monoid M] {s : set M} (hs : is_add_submonoid s) (m : multiset M) :
(∀ (a : M), a ma s)m.sum s

The sum of a multiset of elements of an add_submonoid of an add_comm_monoid is an element of the add_submonoid.

theorem is_add_submonoid.finset_sum_mem {M : Type u_1} {A : Type u_2} [add_comm_monoid M] {s : set M} (hs : is_add_submonoid s) (f : A → M) (t : finset A) :
(∀ (b : A), b tf b s)∑ (b : A) in t, f b s

The sum of elements of an add_submonoid of an add_comm_monoid indexed by a finset is an element of the add_submonoid.

theorem is_submonoid.finset_prod_mem {M : Type u_1} {A : Type u_2} [comm_monoid M] {s : set M} (hs : is_submonoid s) (f : A → M) (t : finset A) :
(∀ (b : A), b tf b s)∏ (b : A) in t, f b s

The product of elements of a submonoid of a comm_monoid indexed by a finset is an element of the submonoid.

inductive add_monoid.in_closure {A : Type u_2} [add_monoid A] (s : set A) :
A → Prop

The inductively defined membership predicate for the submonoid generated by a subset of a monoid.

inductive monoid.in_closure {M : Type u_1} [monoid M] (s : set M) :
M → Prop

The inductively defined membership predicate for the add_submonoid generated by a subset of an add_monoid.

def add_monoid.closure {M : Type u_1} [add_monoid M] (s : set M) :
set M

The inductively defined add_submonoid genrated by a subset of an add_monoid.

def monoid.closure {M : Type u_1} [monoid M] (s : set M) :
set M

The inductively defined submonoid generated by a subset of a monoid.

Equations
theorem monoid.closure.is_submonoid {M : Type u_1} [monoid M] (s : set M) :
theorem add_monoid.subset_closure {M : Type u_1} [add_monoid M] {s : set M} :

A subset of an add_monoid is contained in the add_submonoid it generates.

theorem monoid.subset_closure {M : Type u_1} [monoid M] {s : set M} :

A subset of a monoid is contained in the submonoid it generates.

theorem monoid.closure_subset {M : Type u_1} [monoid M] {s t : set M} (ht : is_submonoid t) (h : s t) :

The submonoid generated by a set is contained in any submonoid that contains the set.

theorem add_monoid.closure_subset {M : Type u_1} [add_monoid M] {s t : set M} (ht : is_add_submonoid t) (h : s t) :

The add_submonoid generated by a set is contained in any add_submonoid that contains the set.

theorem monoid.closure_mono {M : Type u_1} [monoid M] {s t : set M} (h : s t) :

Given subsets t and s of a monoid M, if s ⊆ t, the submonoid of M generated by s is contained in the submonoid generated by t.

theorem add_monoid.closure_mono {M : Type u_1} [add_monoid M] {s t : set M} (h : s t) :

Given subsets t and s of an add_monoid M, if s ⊆ t, the add_submonoid of M generated by s is contained in the add_submonoid generated by t.

theorem monoid.closure_singleton {M : Type u_1} [monoid M] {x : M} :

The submonoid generated by an element of a monoid equals the set of natural number powers of the element.

theorem add_monoid.closure_singleton {M : Type u_1} [add_monoid M] {x : M} :

The add_submonoid generated by an element of an add_monoid equals the set of natural number multiples of the element.

theorem monoid.image_closure {M : Type u_1} [monoid M] {A : Type u_2} [monoid A] {f : M → A} (hf : is_monoid_hom 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 under the monoid hom.

theorem add_monoid.image_closure {M : Type u_1} [add_monoid M] {A : Type u_2} [add_monoid A] {f : M → A} (hf : is_add_monoid_hom 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 under the add_monoid hom.

theorem monoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {a : M} (h : a monoid.closure s) :
∃ (l : list M), (∀ (x : M), x lx s) l.prod = a

Given an element a of the submonoid of a monoid M generated by a set s, there exists a list of elements of s whose product is a.

theorem add_monoid.exists_list_of_mem_closure {M : Type u_1} [add_monoid M] {s : set M} {a : M} (h : a add_monoid.closure s) :
∃ (l : list M), (∀ (x : M), x lx s) l.sum = a

Given an element a of the add_submonoid of an add_monoid M generated by a set s, there exists a list of elements of s whose sum is a.

theorem monoid.mem_closure_union_iff {M : Type u_1} [comm_monoid M] {s t : set M} {x : M} :
x monoid.closure (s t) ∃ (y : M) (H : y monoid.closure s) (z : M) (H : z monoid.closure t), y * z = x

Given sets s, t of a commutative monoid M, x ∈ M is in the submonoid of M generated by s ∪ t iff there exists an element of the submonoid generated by s and an element of the submonoid generated by t whose product is x.

theorem add_monoid.mem_closure_union_iff {M : Type u_1} [add_comm_monoid M] {s t : set M} {x : M} :
x add_monoid.closure (s t) ∃ (y : M) (H : y add_monoid.closure s) (z : M) (H : z add_monoid.closure t), y + z = x

Given sets s, t of a commutative add_monoid M, x ∈ M is in the add_submonoid of M generated by s ∪ t iff there exists an element of the add_submonoid generated by s and an element of the add_submonoid generated by t whose sum is x.

def add_submonoid.of {M : Type u_1} [add_monoid M] {s : set M} (h : is_add_submonoid s) :

Create a bundled additive submonoid from a set s and [is_add_submonoid s].

def submonoid.of {M : Type u_1} [monoid M] {s : set M} (h : is_submonoid s) :

Create a bundled submonoid from a set s and [is_submonoid s].

Equations
theorem submonoid.is_submonoid {M : Type u_1} [monoid M] (S : submonoid M) :