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:
list_prod_mem,multiset_prod_mem,prod_mem: if each element of a collection belongs to a multiplicative submonoid, then so does their product;list_sum_mem,multiset_sum_mem,sum_mem: if each element of a collection belongs to an additive submonoid, then so does their sum;pow_mem,nsmul_mem: ifx ∈ SwhereSis a multiplicative (resp., additive) submonoid andnis a natural number, thenx^n(resp.,n • x) belongs toS;mem_supr_of_directed,coe_supr_of_directed,mem_Sup_of_directed_on,coe_Sup_of_directed_on: the supremum of a directed collection of submonoid is their union.sup_eq_range,mem_sup: supremum of two submonoidsS,Tof a commutative monoid is the set of products;closure_singleton_eq,mem_closure_singleton,mem_closure_pair: the multiplicative (resp., additive) closure of{x}consists of powers (resp., natural multiples) ofx, and a similar result holds for the closure of{x, y}.
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_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) :
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) :
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) :
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) :
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) :
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) :
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
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 ι) :
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) :
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) :
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) :
Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is
in the add_submonoid.
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) :
Sum of elements in an add_submonoid of an add_comm_monoid indexed by a finset
is in the add_submonoid.
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
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} :
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
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) :
↑(has_Sup.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) :
theorem
add_submonoid.mem_sup_left
{M : Type u_1}
[add_zero_class M]
{S T : add_submonoid M}
{x : M} :
theorem
add_submonoid.mem_sup_right
{M : Type u_1}
[add_zero_class M]
{S T : add_submonoid M}
{x : M} :
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) :
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) :
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} :
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 ∈ s → x ∈ has_Sup.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 ∈ s → x ∈ has_Sup.Sup S
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.closure_singleton_eq
{M : Type u_1}
[monoid M]
(x : M) :
submonoid.closure {x} = monoid_hom.mrange (⇑(powers_hom M) x)
theorem
submonoid.mem_closure_singleton_self
{M : Type u_1}
[monoid M]
{y : M} :
y ∈ submonoid.closure {y}
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
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
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
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
The submonoid generated by an element.
Equations
- submonoid.powers n = (monoid_hom.mrange (⇑(powers_hom M) n)).copy (set.range (has_pow.pow n)) _
Instances for submonoid.powers
Instances for ↥submonoid.powers
@[simp]
@[norm_cast]
theorem
submonoid.powers_subset
{M : Type u_1}
[monoid M]
{n : M}
{P : submonoid M}
(h : n ∈ P) :
submonoid.powers n ≤ P
Exponentiation map from natural numbers to powers.
Equations
- submonoid.pow n m = ⇑((⇑(powers_hom M) n).mrange_restrict) (⇑multiplicative.of_add m)
@[simp]
theorem
submonoid.pow_apply
{M : Type u_1}
[monoid M]
(n : M)
(m : ℕ) :
submonoid.pow n m = ⟨n ^ m, _⟩
Logarithms from powers to natural numbers.
Equations
- submonoid.log p = nat.find _
@[simp]
theorem
submonoid.pow_log_eq_self
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(p : ↥(submonoid.powers n)) :
submonoid.pow n (submonoid.log p) = p
theorem
submonoid.pow_right_injective_iff_pow_injective
{M : Type u_1}
[monoid M]
{n : M} :
function.injective (λ (m : ℕ), n ^ m) ↔ function.injective (submonoid.pow 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 : ℕ) :
submonoid.log (submonoid.pow n m) = m
def
submonoid.pow_log_equiv
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ 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
- submonoid.pow_log_equiv h = {to_fun := λ (m : multiplicative ℕ), submonoid.pow n (⇑multiplicative.to_add m), inv_fun := λ (m : ↥(submonoid.powers n)), ⇑multiplicative.of_add (submonoid.log m), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
submonoid.pow_log_equiv_symm_apply
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m))
(m : ↥(submonoid.powers n)) :
⇑((submonoid.pow_log_equiv h).symm) m = ⇑multiplicative.of_add (submonoid.log m)
@[simp]
theorem
submonoid.pow_log_equiv_apply
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m))
(m : multiplicative ℕ) :
⇑(submonoid.pow_log_equiv h) m = submonoid.pow n (⇑multiplicative.to_add m)
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)) :
submonoid.log (x * y) = submonoid.log x + submonoid.log y
theorem
submonoid.log_pow_int_eq_self
{x : ℤ}
(h : 1 < x.nat_abs)
(m : ℕ) :
submonoid.log (submonoid.pow x m) = 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) :
submonoid.map f (submonoid.powers m) = submonoid.powers (⇑f 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
- submonoid.closure_comm_monoid_of_comm hcomm = {mul := monoid.mul (submonoid.closure s).to_monoid, mul_assoc := _, one := monoid.one (submonoid.closure s).to_monoid, one_mul := _, mul_one := _, npow := monoid.npow (submonoid.closure s).to_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
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
- add_submonoid.closure_add_comm_monoid_of_comm hcomm = {add := add_monoid.add (add_submonoid.closure s).to_add_monoid, add_assoc := _, zero := add_monoid.zero (add_submonoid.closure s).to_add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (add_submonoid.closure s).to_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
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) :
is_scalar_tower M N α
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)) :
vadd_assoc_class M N α
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)) :
vadd_comm_class M N α
theorem
add_submonoid.closure_singleton_eq
{A : Type u_2}
[add_monoid A]
(x : A) :
add_submonoid.closure {x} = add_monoid_hom.mrange (⇑(multiples_hom A) x)
The add_submonoid generated by an element of an add_monoid equals the set of
natural number multiples of the element.
theorem
add_submonoid.closure_singleton_zero
{A : Type u_2}
[add_monoid A] :
add_submonoid.closure {0} = ⊥
The additive submonoid generated by an element.
Equations
- add_submonoid.multiples x = (add_monoid_hom.mrange (⇑(multiples_hom A) x)).copy (set.range (λ (i : ℕ), i • x)) _
Instances for ↥add_submonoid.multiples
@[simp]
@[norm_cast]
theorem
add_submonoid.multiples_subset
{M : Type u_1}
[add_monoid M]
{n : M}
{P : add_submonoid M}
(h : n ∈ P) :
@[simp]
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) :
a * b ∈ add_submonoid.closure ↑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.
theorem
mul_mem_class.mul_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 ∈ add_submonoid.closure ↑S) :
a * b ∈ add_submonoid.closure ↑S
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) :
a * 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.
An element is in the closure of a two-element set if it is a linear combination of those two elements.
An element is in the closure of a two-element set if it is a linear combination of those two elements.