mathlib docs: deprecated.submonoid

source

@[class]

structure is_add_submonoid {A : Type u_2} [add_monoid A] :

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.

Instances

source

@[class]

structure is_submonoid {M : Type u_1} [monoid M] :

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.

Instances

source

theorem additive.is_add_submonoid {M : Type u_1} [monoid M] (s : set M) [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_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

@[instance]

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

is_submonoid (s₁ ∩ s₂)

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

Equations

_ = _

source

@[instance]

def is_add_submonoid.inter {M : Type u_1} [add_monoid M] (s₁ s₂ : set M) [is_add_submonoid s₁] [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

@[instance]

def 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.

Equations

_ = _

source

@[instance]

def 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) [∀ (i : ι), is_add_submonoid (s i)] :

(∀ (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) [∀ (i : ι), is_submonoid (s i)] :

(∀ (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 powers {M : Type u_1} [monoid M] :

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

def multiples {A : Type u_2} [add_monoid A] :

A → set A

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

Equations

multiples x = {y : A | ∃ (n : ℕ), n •ℕ x = 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 {A : Type u_2} [add_monoid A] {x : A} :

0 ∈ multiples x

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

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 multiples.self_mem {A : Type u_2} [add_monoid A] {x : A} :

x ∈ multiples x

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

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 {A : Type u_2} [add_monoid A] {x y z : A} :

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

@[instance]

def 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.

Equations

_ = _

source

@[instance]

def 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

@[instance]

def 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

@[instance]

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

is_submonoid set.univ

A monoid is a submonoid of itself.

Equations

univ.is_submonoid = _

source

@[instance]

def preimage.is_add_submonoid {M : Type u_1} [add_monoid M] {N : Type u_2} [add_monoid N] (f : M → N) [is_add_monoid_hom f] (s : set N) [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

@[instance]

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

is_submonoid (f ⁻¹' s)

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

Equations

_ = _

source

@[instance]

theorem image.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] (f : M → γ) [is_add_monoid_hom f] (s : set M) [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

@[instance]

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

is_submonoid (f '' s)

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

source

@[instance]

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

is_submonoid (set.range f)

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

Equations

_ = _

source

@[instance]

def range.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] (f : M → γ) [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_submonoid.pow_mem {M : Type u_1} [monoid M] {s : set M} {a : M} [is_submonoid s] (h : a ∈ s) {n : ℕ} :

a ^ n ∈ s

Submonoids are closed under natural powers.

source

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

n •ℕ a ∈ t

An add_submonoid is closed under multiplication by naturals.

source

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

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.multiple_subset {A : Type u_2} [add_monoid A] {t : set A} {a : A} [is_add_submonoid t] :

a ∈ t → multiples a ⊆ t

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

source

theorem is_submonoid.list_prod_mem {M : Type u_1} [monoid M] {s : set M} [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_add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] {s : set M} [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_add_submonoid.multiset_sum_mem {M : Type u_1} [add_comm_monoid M] (s : set M) [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_submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] (s : set M) [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.finset_sum_mem {M : Type u_1} {A : Type u_2} [add_comm_monoid M] (s : set M) [is_add_submonoid s] (f : A → M) (t : finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → t.sum (λ (b : A), 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) [is_submonoid s] (f : A → M) (t : finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → t.prod (λ (b : A), 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

@[instance]

def subtype.monoid {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

monoid ↥s

Submonoids are themselves monoids.

Equations

subtype.monoid = {mul := λ (x y : ↥s), ⟨↑x * ↑y, _⟩, mul_assoc := _, one := ⟨1, _⟩, one_mul := _, mul_one := _}

source

@[instance]

def subtype.add_monoid {M : Type u_1} [add_monoid M] {s : set M} [is_add_submonoid s] :

add_monoid ↥s

An add_submonoid is itself an add_monoid.

source

@[instance]

def subtype.add_comm_monoid {M : Type u_1} [add_comm_monoid M] {s : set M} [is_add_submonoid s] :

add_comm_monoid ↥s

An add_submonoid of a commutative add_monoid is itself a commutative add_monoid.

source

@[instance]

def subtype.comm_monoid {M : Type u_1} [comm_monoid M] {s : set M} [is_submonoid s] :

comm_monoid ↥s

Submonoids of commutative monoids are themselves commutative monoids.

Equations

subtype.comm_monoid = {mul := monoid.mul subtype.monoid, mul_assoc := _, one := monoid.one subtype.monoid, one_mul := _, mul_one := _, mul_comm := _}

source

@[simp]

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

↑1 = 1

Submonoids inherit the 1 of the monoid.

source

@[simp]

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

↑0 = 0

An add_submonoid inherits the 0 of the add_monoid.

source

@[simp]

theorem is_submonoid.coe_mul {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] (a b : ↥s) :

↑(a * b) = ↑a * ↑b

Submonoids inherit the multiplication of the monoid.

source

@[simp]

theorem is_add_submonoid.coe_add {M : Type u_1} [add_monoid M] {s : set M} [is_add_submonoid s] (a b : ↥s) :

↑(a + b) = ↑a + ↑b

An add_submonoid inherits the addition of the add_monoid.

source

@[simp]

theorem is_submonoid.coe_pow {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] (a : ↥s) (n : ℕ) :

↑(a ^ n) = ↑a ^ n

Submonoids inherit the exponentiation by naturals of the monoid.

source

@[simp]

theorem is_add_submonoid.smul_coe {A : Type u_1} [add_monoid A] {s : set A} [is_add_submonoid s] (a : ↥s) (n : ℕ) :

↑(n •ℕ a) = n •ℕ ↑a

An add_submonoid inherits the multiplication by naturals of the add_monoid.

source

@[instance]

def subtype_val.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

is_monoid_hom subtype.val

The natural injection from a submonoid into the monoid is a monoid hom.

Equations

subtype_val.is_monoid_hom = _

source

@[instance]

def subtype_val.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} [is_add_submonoid s] :

is_add_monoid_hom subtype.val

The natural injection from an add_submonoid into the add_monoid is an add_monoid hom.

source

@[instance]

def coe.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

is_monoid_hom coe

The natural injection from a submonoid into the monoid is a monoid hom.

Equations

coe.is_monoid_hom = subtype_val.is_monoid_hom

source

@[instance]

def coe.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} [is_add_submonoid s] :

is_add_monoid_hom coe

The natural injection from an add_submonoid into the add_monoid is an add_monoid hom.

source

@[instance]

def subtype_mk.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} {γ : Type u_2} [add_monoid γ] [is_add_submonoid s] (f : γ → M) [is_add_monoid_hom f] (h : ∀ (x : γ), f x ∈ s) :

is_add_monoid_hom (λ (x : γ), ⟨f x, _⟩)

Given an add_monoid hom f : γ → M whose image is contained in an add_submonoid s, the induced map from γ to s is an add_monoid hom.

source

@[instance]

def subtype_mk.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} {γ : Type u_2} [monoid γ] [is_submonoid s] (f : γ → M) [is_monoid_hom f] (h : ∀ (x : γ), f x ∈ s) :

is_monoid_hom (λ (x : γ), ⟨f x, _⟩)

Given a monoid hom f : γ → M whose image is contained in a submonoid s, the induced map from γ to s is a monoid hom.

Equations

_ = _

source

@[instance]

def set_inclusion.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} (t : set M) [is_submonoid s] [is_submonoid t] (h : s ⊆ t) :

is_monoid_hom (set.inclusion h)

Given two submonoids s and t such that s ⊆ t, the natural injection from s into t is a monoid hom.

Equations

_ = _

source

@[instance]

def set_inclusion.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} (t : set M) [is_add_submonoid s] [is_add_submonoid t] (h : s ⊆ t) :

is_add_monoid_hom (set.inclusion h)

Given two add_submonoids s and t such that s ⊆ t, the natural injection from s into t is an add_monoid hom.

source

inductive add_monoid.in_closure {A : Type u_2} [add_monoid A] :

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

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 add_submonoid generated by a subset of an add_monoid.

source

def add_monoid.closure {M : Type u_1} [add_monoid M] :

set M → set M

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

source

def monoid.closure {M : Type u_1} [monoid M] :

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

@[instance]

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

is_submonoid (monoid.closure s)

Equations

_ = _

source

@[instance]

def 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 add_monoid.closure_subset {M : Type u_1} [add_monoid M] {s t : set M} [is_add_submonoid t] :

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_subset {M : Type u_1} [monoid M] {s t : set M} [is_submonoid t] :

s ⊆ t → monoid.closure s ⊆ t

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

source

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

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

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 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.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.image_closure {M : Type u_1} [add_monoid M] {A : Type u_2} [add_monoid A] (f : M → A) [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.image_closure {M : Type u_1} [monoid M] {A : Type u_2} [monoid A] (f : M → A) [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 monoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {a : M} :

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

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 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.

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