mathlib3 documentation

group_theory.submonoid.membership

Submonoids: membership criteria #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

submonoid, submonoids

@[simp, norm_cast]
theorem add_submonoid_class.coe_list_sum {M : Type u_1} {B : Type u_3} [add_monoid M] [set_like B M] [add_submonoid_class B M] {S : B} (l : list S) :
@[simp, norm_cast]
theorem submonoid_class.coe_list_prod {M : Type u_1} {B : Type u_3} [monoid M] [set_like B M] [submonoid_class B M] {S : B} (l : list S) :
@[simp, norm_cast]
theorem submonoid_class.coe_multiset_prod {B : Type u_3} {S : B} {M : Type u_1} [comm_monoid M] [set_like B M] [submonoid_class B M] (m : multiset S) :
@[simp, norm_cast]
theorem add_submonoid_class.coe_multiset_sum {B : Type u_3} {S : B} {M : Type u_1} [add_comm_monoid M] [set_like B M] [add_submonoid_class B M] (m : multiset S) :
@[simp, norm_cast]
theorem add_submonoid_class.coe_finset_sum {B : Type u_3} {S : B} {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] [set_like B M] [add_submonoid_class B M] (f : ι S) (s : finset ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp, norm_cast]
theorem submonoid_class.coe_finset_prod {B : Type u_3} {S : B} {ι : Type u_1} {M : Type u_2} [comm_monoid M] [set_like B M] [submonoid_class B M] (f : ι S) (s : finset ι) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem list_prod_mem {M : Type u_1} {B : Type u_3} [monoid M] [set_like B M] [submonoid_class B M] {S : B} {l : list M} (hl : (x : M), x l x S) :
l.prod S

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

theorem list_sum_mem {M : Type u_1} {B : Type u_3} [add_monoid M] [set_like B M] [add_submonoid_class B M] {S : B} {l : list M} (hl : (x : M), x l x S) :
l.sum S

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

theorem multiset_sum_mem {B : Type u_3} {S : B} {M : Type u_1} [add_comm_monoid M] [set_like B M] [add_submonoid_class B M] (m : multiset M) (hm : (a : M), a m a 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 multiset_prod_mem {B : Type u_3} {S : B} {M : Type u_1} [comm_monoid M] [set_like B M] [submonoid_class B M] (m : multiset M) (hm : (a : M), a m a S) :
m.prod S

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

theorem sum_mem {B : Type u_3} {S : B} {M : Type u_1} [add_comm_monoid M] [set_like B M] [add_submonoid_class B M] {ι : Type u_2} {t : finset ι} {f : ι M} (h : (c : ι), c t f c S) :
t.sum (λ (c : ι), 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 prod_mem {B : Type u_3} {S : B} {M : Type u_1} [comm_monoid M] [set_like B M] [submonoid_class B M] {ι : Type u_2} {t : finset ι} {f : ι M} (h : (c : ι), c t f c S) :
t.prod (λ (c : ι), f c) S

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

@[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]
@[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 ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (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 ι) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem submonoid.list_prod_mem {M : Type u_1} [monoid M] (s : submonoid M) {l : list M} (hl : (x : M), x l x 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 l x 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 m a 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 m a 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 submonoid.multiset_noncomm_prod_mem {M : Type u_1} [monoid M] (S : submonoid M) (m : multiset M) (comm : {x : M | x m}.pairwise commute) (h : (x : M), x m x S) :
m.noncomm_prod comm S
theorem add_submonoid.multiset_noncomm_sum_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) (m : multiset M) (comm : {x : M | x m}.pairwise add_commute) (h : (x : M), x m x S) :
m.noncomm_sum comm S
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 t f c S) :
t.sum (λ (c : ι), 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 t f c S) :
t.prod (λ (c : ι), f c) S

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

theorem submonoid.noncomm_prod_mem {M : Type u_1} [monoid M] (S : submonoid M) {ι : Type u_2} (t : finset ι) (f : ι M) (comm : t.pairwise (λ (a b : ι), commute (f a) (f b))) (h : (c : ι), c t f c S) :
t.noncomm_prod f comm S
theorem add_submonoid.noncomm_sum_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {ι : Type u_2} (t : finset ι) (f : ι M) (comm : t.pairwise (λ (a b : ι), add_commute (f a) (f b))) (h : (c : ι), c t f c S) :
t.noncomm_sum f comm 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 has_Sup.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 has_Sup.Sup S (s : add_submonoid M) (H : s S), x 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) :
(has_Sup.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 S x S T
theorem add_submonoid.mem_sup_left {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :
x S x S T
theorem submonoid.mem_sup_right {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x : M} :
x T x S T
theorem add_submonoid.mem_sup_right {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :
x T x 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] {ι : Sort u_2} {S : ι submonoid M} (i : ι) {x : M} :
x S i x supr S
theorem add_submonoid.mem_supr_of_mem {M : Type u_1} [add_zero_class M] {ι : Sort u_2} {S : ι add_submonoid M} (i : ι) {x : M} :
x S i x 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} :
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} :
theorem submonoid.supr_induction {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (S : ι submonoid M) {C : M Prop} {x : M} (hx : x (i : ι), S i) (hp : (i : ι) (x : M), x S i C x) (h1 : C 1) (hmul : (x y : M), C x C y C (x * y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 1 and all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

theorem add_submonoid.supr_induction {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (S : ι add_submonoid M) {C : M Prop} {x : M} (hx : x (i : ι), S i) (hp : (i : ι) (x : M), x S i C x) (h1 : C 0) (hmul : (x y : M), C x C y C (x + y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 0 and all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

theorem submonoid.supr_induction' {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (S : ι submonoid M) {C : Π (x : M), (x (i : ι), S i) Prop} (hp : (i : ι) (x : M) (H : x S i), C x _) (h1 : C 1 _) (hmul : (x y : M) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x * y) _) {x : M} (hx : x (i : ι), S i) :
C x hx

A dependent version of submonoid.supr_induction.

theorem add_submonoid.supr_induction' {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (S : ι add_submonoid M) {C : Π (x : M), (x (i : ι), S i) Prop} (hp : (i : ι) (x : M) (H : x S i), C x _) (h1 : C 0 _) (hmul : (x y : M) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x + y) _) {x : M} (hx : x (i : ι), S i) :
C x hx

A dependent version of add_submonoid.supr_induction.

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 add_submonoid.closure_eq_image_sum {M : Type u_1} [add_monoid M] (s : set M) :
(add_submonoid.closure s) = list.sum '' {l : list M | (x : M), x l x s}
theorem submonoid.closure_eq_image_prod {M : Type u_1} [monoid M] (s : set M) :
(submonoid.closure s) = list.prod '' {l : list M | (x : M), x l x s}
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 l y 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 l y 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 l y 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 l y s), l.prod = x
theorem add_submonoid.closure_induction_left {M : Type u_1} [add_monoid M] {s : set M} {p : M Prop} {x : M} (h : x add_submonoid.closure s) (H1 : p 0) (Hmul : (x : M), x s (y : M), p y p (x + y)) :
p x
theorem submonoid.closure_induction_left {M : Type u_1} [monoid M] {s : set M} {p : M Prop} {x : M} (h : x submonoid.closure s) (H1 : p 1) (Hmul : (x : M), x s (y : M), p y p (x * y)) :
p x
theorem submonoid.induction_of_closure_eq_top_left {M : Type u_1} [monoid M] {s : set M} {p : M Prop} (hs : submonoid.closure s = ) (x : M) (H1 : p 1) (Hmul : (x : M), x s (y : M), p y p (x * y)) :
p x
theorem add_submonoid.induction_of_closure_eq_top_left {M : Type u_1} [add_monoid M] {s : set M} {p : M Prop} (hs : add_submonoid.closure s = ) (x : M) (H1 : p 0) (Hmul : (x : M), x s (y : M), p y p (x + y)) :
p x
theorem submonoid.closure_induction_right {M : Type u_1} [monoid M] {s : set M} {p : M Prop} {x : M} (h : x submonoid.closure s) (H1 : p 1) (Hmul : (x y : M), y s p x p (x * y)) :
p x
theorem add_submonoid.closure_induction_right {M : Type u_1} [add_monoid M] {s : set M} {p : M Prop} {x : M} (h : x add_submonoid.closure s) (H1 : p 0) (Hmul : (x y : M), y s p x p (x + y)) :
p x
theorem submonoid.induction_of_closure_eq_top_right {M : Type u_1} [monoid M] {s : set M} {p : M Prop} (hs : submonoid.closure s = ) (x : M) (H1 : p 1) (Hmul : (x y : M), y s p x p (x * y)) :
p x
theorem add_submonoid.induction_of_closure_eq_top_right {M : Type u_1} [add_monoid M] {s : set M} {p : M Prop} (hs : add_submonoid.closure s = ) (x : M) (H1 : p 0) (Hmul : (x y : M), y s p x p (x + y)) :
p x
@[simp]
theorem submonoid.mem_powers {M : Type u_1} [monoid M] (n : M) :
@[norm_cast]
theorem submonoid.coe_powers {M : Type u_1} [monoid M] (x : M) :
(submonoid.powers x) = set.range (λ (n : ), x ^ n)
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_subset {M : Type u_1} [monoid M] {n : M} {P : submonoid M} (h : n P) :
@[simp]
theorem submonoid.powers_one {M : Type u_1} [monoid M] :
def submonoid.pow {M : Type u_1} [monoid M] (n : M) (m : ) :

Exponentiation map from natural numbers to powers.

Equations
@[simp]
theorem submonoid.pow_coe {M : Type u_1} [monoid M] (n : M) (m : ) :
(submonoid.pow n m) = n ^ m
theorem submonoid.pow_apply {M : Type u_1} [monoid M] (n : M) (m : ) :
submonoid.pow n m = n ^ m, _⟩
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)) :
@[simp]
theorem submonoid.log_pow_eq_self {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (h : function.injective (λ (m : ), n ^ m)) (m : ) :

The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers when it is injective. The inverse is given by the logarithms.

Equations
theorem submonoid.log_mul {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (h : function.injective (λ (m : ), n ^ m)) (x y : (submonoid.powers n)) :
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} {F : Type u_3} [monoid N] [monoid_hom_class F M N] (f : F) (m : M) :
def submonoid.closure_comm_monoid_of_comm {M : Type u_1} [monoid M] {s : set M} (hcomm : (a : M), a s (b : M), b s a * b = b * a) :

If all the elements of a set s commute, then closure s is a commutative monoid.

Equations
def add_submonoid.closure_add_comm_monoid_of_comm {M : Type u_1} [add_monoid M] {s : set M} (hcomm : (a : M), a s (b : M), b s a + b = b + a) :

If all the elements of a set s commute, then closure s forms an additive commutative monoid.

Equations
theorem is_scalar_tower.of_mclosure_eq_top {M : Type u_1} {N : Type u_2} {α : Type u_3} [monoid M] [mul_action M N] [has_smul N α] [mul_action M α] {s : set M} (htop : submonoid.closure s = ) (hs : (x : M), x s (y : N) (z : α), (x y) z = x y z) :
theorem vadd_assoc_class.of_mclosure_eq_top {M : Type u_1} {N : Type u_2} {α : Type u_3} [add_monoid M] [add_action M N] [has_vadd N α] [add_action M α] {s : set M} (htop : add_submonoid.closure s = ) (hs : (x : M), x s (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)) :
theorem vadd_comm_class.of_mclosure_eq_top {M : Type u_1} {N : Type u_2} {α : Type u_3} [add_monoid M] [has_vadd N α] [add_action M α] {s : set M} (htop : add_submonoid.closure s = ) (hs : (x : M), x s (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)) :
theorem smul_comm_class.of_mclosure_eq_top {M : Type u_1} {N : Type u_2} {α : Type u_3} [monoid M] [has_smul N α] [mul_action M α] {s : set M} (htop : submonoid.closure s = ) (hs : (x : M), x s (y : N) (z : α), x y z = y x z) :
theorem submonoid.mem_sup {N : Type u_4} [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_4} [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} :

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
Instances for add_submonoid.multiples
@[simp]
@[norm_cast]
theorem add_submonoid.coe_multiples {M : Type u_1} [add_monoid M] (x : M) :
theorem add_submonoid.mem_multiples_iff {M : Type u_1} [add_monoid M] (x z : M) :
theorem add_submonoid.multiples_subset {M : Type u_1} [add_monoid M] {n : M} {P : add_submonoid M} (h : n P) :

Lemmas about additive closures of subsemigroup.

theorem mul_mem_class.mul_right_mem_add_closure {M : Type u_1} {R : Type u_4} [non_unital_non_assoc_semiring R] [set_like M R] [mul_mem_class M R] {S : M} {a b : R} (ha : a add_submonoid.closure S) (hb : b S) :

The product of an element of the additive closure of a multiplicative subsemigroup 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 mul_mem_class.mul_left_mem_add_closure {M : Type u_1} {R : Type u_4} [non_unital_non_assoc_semiring R] [set_like M R] [mul_mem_class M R] {S : M} {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.

theorem add_submonoid.mem_closure_pair {A : Type u_1} [add_comm_monoid A] (a b c : A) :
c add_submonoid.closure {a, b} (m n : ), m a + n b = c

An element is in the closure of a two-element set if it is a linear combination of those two elements.

theorem submonoid.mem_closure_pair {A : Type u_1} [comm_monoid A] (a b c : A) :
c submonoid.closure {a, b} (m n : ), a ^ m * b ^ n = c

An element is in the closure of a two-element set if it is a linear combination of those two elements.