deprecated.submonoid - mathlib docs

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 ∈ s → b ∈ s → a + 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.

source

structure is_submonoid {M : Type u_1} [monoid M] (s : set M) :

Prop

one_mem : 1 ∈ s
mul_mem : ∀ {a b : M}, a ∈ s → b ∈ s → a * 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.

source

theorem additive.is_add_submonoid {M : Type u_1} [monoid M] {s : set M} (is : is_submonoid s) :

is_add_submonoid s

source

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

is_add_submonoid s ↔ is_submonoid s

source

theorem multiplicative.is_submonoid {A : Type u_2} [add_monoid A] {s : set A} (is : is_add_submonoid s) :

is_submonoid s

source

theorem multiplicative.is_submonoid_iff {A : Type u_2} [add_monoid A] {s : set A} :

is_submonoid s ↔ is_add_submonoid s

source

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.

source

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.

source

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

is_submonoid (set.Inter s)

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

source

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)) :

is_add_submonoid (set.Inter s)

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

source

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.

source

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.

source

def multiples {M : Type u_1} [add_monoid M] (x : M) :

set M

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

Equations

multiples x = {y : M | ∃ (n : ℕ), n • x = y}

source

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

powers x = {y : M | ∃ (n : ℕ), x ^ n = y}

source

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

1 ∈ powers x

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

source

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

0 ∈ multiples x

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

source

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

x ∈ multiples x

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

source

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

x ∈ powers x

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

source

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

y ∈ powers x → z ∈ powers x → y * z ∈ powers x

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

source

theorem multiples.add_mem {M : Type u_1} [add_monoid M] {x y z : M} :

y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x

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

source

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

is_add_submonoid (multiples x)

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

source

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

is_submonoid (powers x)

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

source

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

is_submonoid set.univ

A monoid is a submonoid of itself.

source

theorem univ.is_add_submonoid {M : Type u_1} [add_monoid M] :

is_add_submonoid set.univ

An add_monoid is an add_submonoid of itself.

source

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) :

is_add_submonoid (f ⁻¹' s)

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

source

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) :

is_submonoid (f ⁻¹' s)

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

source

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) :

is_submonoid (f '' s)

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

source

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) :

is_add_submonoid (f '' s)

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

source

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

is_submonoid (set.range f)

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

source

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) :

is_add_submonoid (set.range f)

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

source

theorem is_add_submonoid.smul_mem {M : Type u_1} [add_monoid M] {s : set M} {a : M} (hs : is_add_submonoid s) (h : a ∈ s) {n : ℕ} :

n • a ∈ s

An add_submonoid is closed under multiplication by naturals.

source

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.

source

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

powers a ⊆ s

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

source

theorem is_add_submonoid.multiples_subset {M : Type u_1} [add_monoid M] {s : set M} {a : M} (hs : is_add_submonoid s) (h : a ∈ s) :

multiples a ⊆ s

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

source

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 ∈ l → x ∈ s) → l.sum ∈ s

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

source

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 ∈ l → x ∈ s) → l.prod ∈ s

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

source

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 ∈ m → a ∈ s) → m.prod ∈ s

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

source

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 ∈ m → a ∈ 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.

source

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 ∈ t → f 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.

source

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 ∈ t → f 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.

source

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

A → Prop

basic : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A} {a : A}, a ∈ s → add_monoid.in_closure s a
zero : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A}, add_monoid.in_closure s 0
add : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A} {a b : A}, add_monoid.in_closure s a → add_monoid.in_closure s b → add_monoid.in_closure s (a + b)

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

source

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

M → Prop

basic : ∀ {M : Type u_1} [_inst_1 : monoid M] {s : set M} {a : M}, a ∈ s → monoid.in_closure s a
one : ∀ {M : Type u_1} [_inst_1 : monoid M] {s : set M}, monoid.in_closure s 1
mul : ∀ {M : Type u_1} [_inst_1 : monoid M] {s : set M} {a b : M}, monoid.in_closure s a → monoid.in_closure s b → monoid.in_closure s (a * b)

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

source

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.

Equations

add_monoid.closure s = {a : M | add_monoid.in_closure s a}

source

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

monoid.closure s = {a : M | monoid.in_closure s a}

source

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

is_submonoid (monoid.closure s)

source

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

is_add_submonoid (add_monoid.closure s)

source

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

s ⊆ add_monoid.closure s

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

source

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

s ⊆ monoid.closure s

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

source

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

monoid.closure s ⊆ t

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

source

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

add_monoid.closure s ⊆ t

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

source

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

monoid.closure s ⊆ monoid.closure 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.

source

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

add_monoid.closure s ⊆ add_monoid.closure 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.

source

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

monoid.closure {x} = powers x

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

source

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

add_monoid.closure {x} = multiples x

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

source

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) :

f '' monoid.closure s = monoid.closure (f '' s)

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.

source

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) :

f '' add_monoid.closure s = add_monoid.closure (f '' s)

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.

source

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 ∈ l → x ∈ 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.

source

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 ∈ l → x ∈ 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.

source

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.

source

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.