mathlib documentation

group_theory.submonoid.membership

Submonoids: membership criteria #

In this file we prove various facts about membership in a submonoid:

Tags #

submonoid, submonoids

@[simp, norm_cast]
theorem add_submonoid.coe_nsmul {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x : S) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem submonoid.coe_pow {M : Type u_1} [monoid M] (S : submonoid M) (x : S) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem add_submonoid.coe_list_sum {M : Type u_1} [add_monoid M] (S : add_submonoid M) (l : list S) :
@[simp, norm_cast]
theorem submonoid.coe_list_prod {M : Type u_1} [monoid M] (S : submonoid M) (l : list S) :
@[simp, norm_cast]
theorem add_submonoid.coe_multiset_sum {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (m : multiset S) :
@[simp, norm_cast]
theorem submonoid.coe_multiset_prod {M : Type u_1} [comm_monoid M] (S : submonoid M) (m : multiset S) :
@[simp, norm_cast]
theorem add_submonoid.coe_finset_sum {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] (S : add_submonoid M) (f : ι → S) (s : finset ι) :
∑ (i : ι) in s, f i = ∑ (i : ι) in s, (f i)
@[simp, norm_cast]
theorem submonoid.coe_finset_prod {ι : Type u_1} {M : Type u_2} [comm_monoid M] (S : submonoid M) (f : ι → S) (s : finset ι) :
∏ (i : ι) in s, f i = ∏ (i : ι) in s, (f i)
theorem submonoid.list_prod_mem {M : Type u_1} [monoid M] (S : submonoid M) {l : list M} (hl : ∀ (x : M), x lx S) :
l.prod S

Product of a list of elements in a submonoid is in the submonoid.

theorem add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {l : list M} (hl : ∀ (x : M), x lx S) :
l.sum S

Sum of a list of elements in an add_submonoid is in the add_submonoid.

theorem submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) (m : multiset M) (hm : ∀ (a : M), a ma S) :
m.prod S

Product of a multiset of elements in a submonoid of a comm_monoid is in the submonoid.

theorem add_submonoid.multiset_sum_mem {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (m : multiset M) (hm : ∀ (a : M), a ma S) :
m.sum S

Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is in the add_submonoid.

theorem add_submonoid.sum_mem {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} (h : ∀ (c : ι), c tf c S) :
∑ (c : ι) in t, f c S

Sum of elements in an add_submonoid of an add_comm_monoid indexed by a finset is in the add_submonoid.

theorem submonoid.prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} (h : ∀ (c : ι), c tf c S) :
∏ (c : ι) in t, f c S

Product of elements of a submonoid of a comm_monoid indexed by a finset is in the submonoid.

theorem submonoid.pow_mem {M : Type u_1} [monoid M] (S : submonoid M) {x : M} (hx : x S) (n : ) :
x ^ n S
theorem add_submonoid.nsmul_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {x : M} (hx : x S) (n : ) :
n x S
theorem add_submonoid.mem_supr_of_directed {M : Type u_1} [add_zero_class M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → add_submonoid M} (hS : directed has_le.le S) {x : M} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i
theorem submonoid.mem_supr_of_directed {M : Type u_1} [mul_one_class M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → submonoid M} (hS : directed has_le.le S) {x : M} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i
theorem add_submonoid.coe_supr_of_directed {M : Type u_1} [add_zero_class M] {ι : Sort u_2} [nonempty ι] {S : ι → add_submonoid M} (hS : directed has_le.le S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem submonoid.coe_supr_of_directed {M : Type u_1} [mul_one_class M] {ι : Sort u_2} [nonempty ι] {S : ι → submonoid M} (hS : directed has_le.le S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem submonoid.mem_Sup_of_directed_on {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : M} :
x Sup S ∃ (s : submonoid M) (H : s S), x s
theorem add_submonoid.mem_Sup_of_directed_on {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : M} :
x Sup S ∃ (s : add_submonoid M) (H : s S), x s
theorem add_submonoid.coe_Sup_of_directed_on {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) :
(Sup S) = ⋃ (s : add_submonoid M) (H : s S), s
theorem submonoid.coe_Sup_of_directed_on {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) :
(Sup S) = ⋃ (s : submonoid M) (H : s S), s
theorem submonoid.mem_sup_left {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x : M} :
x Sx S T
theorem add_submonoid.mem_sup_left {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :
x Sx S T
theorem submonoid.mem_sup_right {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x : M} :
x Tx S T
theorem add_submonoid.mem_sup_right {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :
x Tx S T
theorem add_submonoid.add_mem_sup {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x y : M} (hx : x S) (hy : y T) :
x + y S T
theorem submonoid.mul_mem_sup {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x y : M} (hx : x S) (hy : y T) :
x * y S T
theorem submonoid.mem_supr_of_mem {M : Type u_1} [mul_one_class M] {ι : Type u_2} {S : ι → submonoid M} (i : ι) {x : M} :
x S ix supr S
theorem add_submonoid.mem_supr_of_mem {M : Type u_1} [add_zero_class M] {ι : Type u_2} {S : ι → add_submonoid M} (i : ι) {x : M} :
x S ix supr S
theorem add_submonoid.mem_Sup_of_mem {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} {s : add_submonoid M} (hs : s S) {x : M} :
x sx Sup S
theorem submonoid.mem_Sup_of_mem {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} {s : submonoid M} (hs : s S) {x : M} :
x sx Sup S
theorem submonoid.closure_singleton_eq {M : Type u_1} [monoid M] (x : M) :
theorem submonoid.mem_closure_singleton {M : Type u_1} [monoid M] {x y : M} :
y submonoid.closure {x} ∃ (n : ), x ^ n = y

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

theorem submonoid.mem_closure_singleton_self {M : Type u_1} [monoid M] {y : M} :
theorem submonoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {x : M} (hx : x submonoid.closure s) :
∃ (l : list M) (hl : ∀ (y : M), y ly s), l.prod = x
theorem add_submonoid.exists_list_of_mem_closure {M : Type u_1} [add_monoid M] {s : set M} {x : M} (hx : x add_submonoid.closure s) :
∃ (l : list M) (hl : ∀ (y : M), y ly s), l.sum = x
theorem add_submonoid.exists_multiset_of_mem_closure {M : Type u_1} [add_comm_monoid M] {s : set M} {x : M} (hx : x add_submonoid.closure s) :
∃ (l : multiset M) (hl : ∀ (y : M), y ly s), l.sum = x
theorem submonoid.exists_multiset_of_mem_closure {M : Type u_1} [comm_monoid M] {s : set M} {x : M} (hx : x submonoid.closure s) :
∃ (l : multiset M) (hl : ∀ (y : M), y ly s), l.prod = x
def submonoid.powers {M : Type u_1} [monoid M] (n : M) :

The submonoid generated by an element.

Equations
@[simp]
theorem submonoid.mem_powers {M : Type u_1} [monoid M] (n : M) :
theorem submonoid.mem_powers_iff {M : Type u_1} [monoid M] (x z : M) :
x submonoid.powers z ∃ (n : ), z ^ n = x
theorem submonoid.powers_eq_closure {M : Type u_1} [monoid M] (n : M) :
theorem submonoid.powers_subset {M : Type u_1} [monoid M] {n : M} {P : submonoid M} (h : n P) :
def submonoid.pow {M : Type u_1} [monoid M] (n : M) (m : ) :

Exponentiation map from natural numbers to powers.

Equations
def submonoid.log {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (p : (submonoid.powers n)) :

Logarithms from powers to natural numbers.

Equations
@[simp]
theorem submonoid.pow_log_eq_self {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (p : (submonoid.powers n)) :
theorem submonoid.log_pow_eq_self {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (h : function.injective (λ (m : ), n ^ m)) (m : ) :
theorem submonoid.log_pow_int_eq_self {x : } (h : 1 < x.nat_abs) (m : ) :
@[simp]
theorem submonoid.map_powers {M : Type u_1} [monoid M] {N : Type u_2} [monoid N] (f : M →* N) (m : M) :
theorem add_submonoid.sup_eq_range {N : Type u_3} [add_comm_monoid N] (s t : add_submonoid N) :
theorem submonoid.sup_eq_range {N : Type u_3} [comm_monoid N] (s t : submonoid N) :
theorem submonoid.mem_sup {N : Type u_3} [comm_monoid N] {s t : submonoid N} {x : N} :
x s t ∃ (y : N) (H : y s) (z : N) (H : z t), y * z = x
theorem add_submonoid.mem_sup {N : Type u_3} [add_comm_monoid N] {s t : add_submonoid N} {x : N} :
x s t ∃ (y : N) (H : y s) (z : N) (H : z t), y + z = x
theorem add_submonoid.mem_closure_singleton {A : Type u_2} [add_monoid A] {x y : A} :
y add_submonoid.closure {x} ∃ (n : ), n x = y

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

def add_submonoid.multiples {A : Type u_2} [add_monoid A] (x : A) :

The additive submonoid generated by an element.

Equations
@[simp]
theorem add_submonoid.mem_multiples {A : Type u_2} [add_monoid A] (x : A) :
theorem add_submonoid.mem_multiples_iff {A : Type u_2} [add_monoid A] (x z : A) :
x add_submonoid.multiples z ∃ (n : ), n z = x
theorem add_submonoid.multiples_subset {A : Type u_2} [add_monoid A] {x : A} {P : add_submonoid A} (h : x P) :

Lemmas about additive closures of submonoid.

theorem submonoid.mul_right_mem_add_closure {R : Type u_3} [non_assoc_semiring R] (S : submonoid R) {a b : R} (ha : a add_submonoid.closure S) (hb : b S) :

The product of an element of the additive closure of a multiplicative submonoid M and an element of M is contained in the additive closure of M.

The product of two elements of the additive closure of a submonoid M is an element of the additive closure of M.

theorem submonoid.mul_left_mem_add_closure {R : Type u_3} [non_assoc_semiring R] (S : submonoid R) {a b : R} (ha : a S) (hb : b add_submonoid.closure S) :

The product of an element of S and an element of the additive closure of a multiplicative submonoid S is contained in the additive closure of S.