# Submonoids: membership criteria #

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: if x ∈ S where S is a multiplicative (resp., additive) submonoid and n is a natural number, then x^n (resp., n • x) belongs to S;
• mem_iSup_of_directed, coe_iSup_of_directed, mem_sSup_of_directedOn, coe_sSup_of_directedOn: the supremum of a directed collection of submonoid is their union.
• sup_eq_range, mem_sup: supremum of two submonoids S, T of 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) of x, and a similar result holds for the closure of {x, y}.

## Tags #

submonoid, submonoids

@[simp]
theorem AddSubmonoidClass.coe_list_sum {M : Type u_1} {B : Type u_3} [] [SetLike B M] [] {S : B} (l : List S) :
() = List.sum (List.map Subtype.val l)
@[simp]
theorem SubmonoidClass.coe_list_prod {M : Type u_1} {B : Type u_3} [] [SetLike B M] [] {S : B} (l : List S) :
() = List.prod (List.map Subtype.val l)
@[simp]
theorem AddSubmonoidClass.coe_multiset_sum {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] (m : Multiset S) :
() = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem SubmonoidClass.coe_multiset_prod {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] (m : Multiset S) :
() = Multiset.prod (Multiset.map Subtype.val m)
theorem AddSubmonoidClass.coe_finset_sum {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [] [SetLike B M] [] (f : ιS) (s : ) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (f i)
theorem SubmonoidClass.coe_finset_prod {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [] [SetLike B M] [] (f : ιS) (s : ) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (f i)
theorem list_sum_mem {M : Type u_1} {B : Type u_3} [] [SetLike B M] [] {S : B} {l : List M} (hl : xl, x S) :
S

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

theorem list_prod_mem {M : Type u_1} {B : Type u_3} [] [SetLike B M] [] {S : B} {l : List M} (hl : xl, x S) :
S

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

theorem multiset_sum_mem {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] (m : ) (hm : am, a S) :

Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is in the AddSubmonoid.

theorem multiset_prod_mem {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] (m : ) (hm : am, a S) :

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

abbrev sum_mem.match_1 {M : Type u_2} {ι : Type u_1} {t : } {f : ιM} (_x : M) (motive : (∃ a ∈ t.val, f a = _x)Prop) :
∀ (x : ∃ a ∈ t.val, f a = _x), (∀ (i : ι) (hi : i t.val) (hix : f i = _x), motive (_ : ∃ a ∈ t.val, f a = _x))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem sum_mem {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] {ι : Type u_5} {t : } {f : ιM} (h : ct, f c S) :
(Finset.sum t fun (c : ι) => f c) S

Sum of elements in an AddSubmonoid of an AddCommMonoid indexed by a Finset is in the AddSubmonoid.

theorem prod_mem {B : Type u_3} {S : B} {M : Type u_4} [] [SetLike B M] [] {ι : Type u_5} {t : } {f : ιM} (h : ct, f c S) :
(Finset.prod t fun (c : ι) => f c) S

Product of elements of a submonoid of a CommMonoid indexed by a Finset is in the submonoid.

theorem AddSubmonoid.coe_list_sum {M : Type u_1} [] (s : ) (l : List s) :
() = List.sum (List.map Subtype.val l)
theorem Submonoid.coe_list_prod {M : Type u_1} [] (s : ) (l : List s) :
() = List.prod (List.map Subtype.val l)
theorem AddSubmonoid.coe_multiset_sum {M : Type u_4} [] (S : ) (m : Multiset S) :
() = Multiset.sum (Multiset.map Subtype.val m)
theorem Submonoid.coe_multiset_prod {M : Type u_4} [] (S : ) (m : Multiset S) :
() = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem AddSubmonoid.coe_finset_sum {ι : Type u_4} {M : Type u_5} [] (S : ) (f : ιS) (s : ) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (f i)
@[simp]
theorem Submonoid.coe_finset_prod {ι : Type u_4} {M : Type u_5} [] (S : ) (f : ιS) (s : ) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (f i)
theorem AddSubmonoid.list_sum_mem {M : Type u_1} [] (s : ) {l : List M} (hl : xl, x s) :
s

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

theorem Submonoid.list_prod_mem {M : Type u_1} [] (s : ) {l : List M} (hl : xl, x s) :
s

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

theorem AddSubmonoid.multiset_sum_mem {M : Type u_4} [] (S : ) (m : ) (hm : am, a S) :

Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is in the AddSubmonoid.

theorem Submonoid.multiset_prod_mem {M : Type u_4} [] (S : ) (m : ) (hm : am, a S) :

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

theorem AddSubmonoid.multiset_noncommSum_mem {M : Type u_1} [] (S : ) (m : ) (comm : Set.Pairwise {x : M | x m} AddCommute) (h : xm, x S) :
theorem Submonoid.multiset_noncommProd_mem {M : Type u_1} [] (S : ) (m : ) (comm : Set.Pairwise {x : M | x m} Commute) (h : xm, x S) :
theorem AddSubmonoid.sum_mem {M : Type u_4} [] (S : ) {ι : Type u_5} {t : } {f : ιM} (h : ct, f c S) :
(Finset.sum t fun (c : ι) => f c) S

Sum of elements in an AddSubmonoid of an AddCommMonoid indexed by a Finset is in the AddSubmonoid.

theorem Submonoid.prod_mem {M : Type u_4} [] (S : ) {ι : Type u_5} {t : } {f : ιM} (h : ct, f c S) :
(Finset.prod t fun (c : ι) => f c) S

Product of elements of a submonoid of a CommMonoid indexed by a Finset is in the submonoid.

theorem AddSubmonoid.noncommSum_mem {M : Type u_1} [] (S : ) {ι : Type u_4} (t : ) (f : ιM) (comm : Set.Pairwise t fun (a b : ι) => AddCommute (f a) (f b)) (h : ct, f c S) :
theorem Submonoid.noncommProd_mem {M : Type u_1} [] (S : ) {ι : Type u_4} (t : ) (f : ιM) (comm : Set.Pairwise t fun (a b : ι) => Commute (f a) (f b)) (h : ct, f c S) :
abbrev AddSubmonoid.mem_iSup_of_directed.match_1 {M : Type u_2} [] {ι : Sort u_1} {S : ι} {x : M} (motive : (∃ (i : ι), x S i)Prop) :
∀ (x_1 : ∃ (i : ι), x S i), (∀ (i : ι) (hi : x S i), motive (_ : ∃ (i : ι), x S i))motive x_1
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem AddSubmonoid.mem_iSup_of_directed {M : Type u_1} [] {ι : Sort u_4} [hι : ] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) S) {x : M} :
x ⨆ (i : ι), S i ∃ (i : ι), x S i
theorem Submonoid.mem_iSup_of_directed {M : Type u_1} [] {ι : Sort u_4} [hι : ] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) S) {x : M} :
x ⨆ (i : ι), S i ∃ (i : ι), x S i
theorem AddSubmonoid.coe_iSup_of_directed {M : Type u_1} [] {ι : Sort u_4} [] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem Submonoid.coe_iSup_of_directed {M : Type u_1} [] {ι : Sort u_4} [] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem AddSubmonoid.mem_sSup_of_directedOn {M : Type u_1} [] {S : Set ()} (Sne : ) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) {x : M} :
x sSup S ∃ s ∈ S, x s
theorem Submonoid.mem_sSup_of_directedOn {M : Type u_1} [] {S : Set ()} (Sne : ) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) {x : M} :
x sSup S ∃ s ∈ S, x s
theorem AddSubmonoid.coe_sSup_of_directedOn {M : Type u_1} [] {S : Set ()} (Sne : ) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) :
(sSup S) = ⋃ s ∈ S, s
theorem Submonoid.coe_sSup_of_directedOn {M : Type u_1} [] {S : Set ()} (Sne : ) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) :
(sSup S) = ⋃ s ∈ S, s
theorem AddSubmonoid.mem_sup_left {M : Type u_1} [] {S : } {T : } {x : M} :
x Sx S T
theorem Submonoid.mem_sup_left {M : Type u_1} [] {S : } {T : } {x : M} :
x Sx S T
theorem AddSubmonoid.mem_sup_right {M : Type u_1} [] {S : } {T : } {x : M} :
x Tx S T
theorem Submonoid.mem_sup_right {M : Type u_1} [] {S : } {T : } {x : M} :
x Tx S T
theorem AddSubmonoid.add_mem_sup {M : Type u_1} [] {S : } {T : } {x : M} {y : M} (hx : x S) (hy : y T) :
x + y S T
theorem Submonoid.mul_mem_sup {M : Type u_1} [] {S : } {T : } {x : M} {y : M} (hx : x S) (hy : y T) :
x * y S T
theorem AddSubmonoid.mem_iSup_of_mem {M : Type u_1} [] {ι : Sort u_4} {S : ι} (i : ι) {x : M} :
x S ix iSup S
theorem Submonoid.mem_iSup_of_mem {M : Type u_1} [] {ι : Sort u_4} {S : ι} (i : ι) {x : M} :
x S ix iSup S
theorem AddSubmonoid.mem_sSup_of_mem {M : Type u_1} [] {S : Set ()} {s : } (hs : s S) {x : M} :
x sx sSup S
theorem Submonoid.mem_sSup_of_mem {M : Type u_1} [] {S : Set ()} {s : } (hs : s S) {x : M} :
x sx sSup S
theorem AddSubmonoid.iSup_induction {M : Type u_1} [] {ι : Sort u_4} (S : ι) {C : MProp} {x : M} (hx : x ⨆ (i : ι), S i) (hp : ∀ (i : ι), xS i, C x) (h1 : C 0) (hmul : ∀ (x y : M), C xC yC (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.iSup_induction {M : Type u_1} [] {ι : Sort u_4} (S : ι) {C : MProp} {x : M} (hx : x ⨆ (i : ι), S i) (hp : ∀ (i : ι), xS i, C x) (h1 : C 1) (hmul : ∀ (x y : M), C xC yC (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 AddSubmonoid.iSup_induction' {M : Type u_1} [] {ι : Sort u_4} (S : ι) {C : (x : M) → x ⨆ (i : ι), S iProp} (hp : ∀ (i : ι) (x : M) (hxS : x S i), C x (_ : x ⨆ (i : ι), S i)) (h1 : C 0 (_ : 0 ⨆ (i : ι), S i)) (hmul : ∀ (x y : M) (hx : x ⨆ (i : ι), S i) (hy : y ⨆ (i : ι), S i), C x hxC y hyC (x + y) (_ : x + y ⨆ (i : ι), S i)) {x : M} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of AddSubmonoid.iSup_induction.

theorem Submonoid.iSup_induction' {M : Type u_1} [] {ι : Sort u_4} (S : ι) {C : (x : M) → x ⨆ (i : ι), S iProp} (hp : ∀ (i : ι) (x : M) (hxS : x S i), C x (_ : x ⨆ (i : ι), S i)) (h1 : C 1 (_ : 1 ⨆ (i : ι), S i)) (hmul : ∀ (x y : M) (hx : x ⨆ (i : ι), S i) (hy : y ⨆ (i : ι), S i), C x hxC y hyC (x * y) (_ : x * y ⨆ (i : ι), S i)) {x : M} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of Submonoid.iSup_induction.

theorem Submonoid.closure_singleton_eq {M : Type u_1} [] (x : M) :
theorem Submonoid.mem_closure_singleton {M : Type u_1} [] {x : M} {y : M} :
y ∃ (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} [] {y : M} :
y
abbrev AddSubmonoid.card_bot.match_1 {M : Type u_1} [] (motive : Prop) :
∀ (x : ), (∀ (_y : M) (hy : _y ), motive { val := _y, property := hy })motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem AddSubmonoid.card_bot {M : Type u_1} [] :
∀ {x : },
theorem Submonoid.card_bot {M : Type u_1} [] :
∀ {x : },
theorem AddSubmonoid.eq_bot_of_card_le {M : Type u_1} [] {S : } [Fintype S] (h : 1) :
S =
theorem Submonoid.eq_bot_of_card_le {M : Type u_1} [] {S : } [Fintype S] (h : 1) :
S =
theorem AddSubmonoid.eq_bot_of_card_eq {M : Type u_1} [] {S : } [Fintype S] (h : = 1) :
S =
theorem Submonoid.eq_bot_of_card_eq {M : Type u_1} [] {S : } [Fintype S] (h : = 1) :
S =
theorem AddSubmonoid.card_le_one_iff_eq_bot {M : Type u_1} [] {S : } [Fintype S] :
1 S =
theorem Submonoid.card_le_one_iff_eq_bot {M : Type u_1} [] {S : } [Fintype S] :
1 S =
theorem AddSubmonoid.eq_bot_iff_card {M : Type u_1} [] {S : } [Fintype S] :
S = = 1
theorem Submonoid.eq_bot_iff_card {M : Type u_1} [] {S : } [Fintype S] :
S = = 1
theorem FreeAddMonoid.mrange_lift {M : Type u_1} [] {α : Type u_4} (f : αM) :
theorem FreeMonoid.mrange_lift {M : Type u_1} [] {α : Type u_4} (f : αM) :
MonoidHom.mrange (FreeMonoid.lift f) =
theorem AddSubmonoid.closure_eq_mrange {M : Type u_1} [] (s : Set M) :
theorem Submonoid.closure_eq_mrange {M : Type u_1} [] (s : Set M) :
= MonoidHom.mrange (FreeMonoid.lift Subtype.val)
theorem AddSubmonoid.closure_eq_image_sum {M : Type u_1} [] (s : Set M) :
= List.sum '' {l : List M | xl, x s}
theorem Submonoid.closure_eq_image_prod {M : Type u_1} [] (s : Set M) :
= List.prod '' {l : List M | xl, x s}
theorem AddSubmonoid.exists_list_of_mem_closure {M : Type u_1} [] {s : Set M} {x : M} (hx : ) :
∃ (l : List M), (yl, y s) = x
theorem Submonoid.exists_list_of_mem_closure {M : Type u_1} [] {s : Set M} {x : M} (hx : ) :
∃ (l : List M), (yl, y s) = x
theorem AddSubmonoid.exists_multiset_of_mem_closure {M : Type u_4} [] {s : Set M} {x : M} (hx : ) :
∃ (l : ) (_ : yl, y s),
theorem Submonoid.exists_multiset_of_mem_closure {M : Type u_4} [] {s : Set M} {x : M} (hx : ) :
∃ (l : ) (_ : yl, y s),
theorem AddSubmonoid.closure_induction_left {M : Type u_1} [] {s : Set M} {p : (m : M) → } (one : p 0 (_ : )) (mul_left : ∀ (x : M) (hx : x s) (y : M) (hy : ), p y hyp (x + y) (_ : x + y )) {x : M} (h : ) :
p x h
theorem Submonoid.closure_induction_left {M : Type u_1} [] {s : Set M} {p : (m : M) → Prop} (one : p 1 (_ : )) (mul_left : ∀ (x : M) (hx : x s) (y : M) (hy : ), p y hyp (x * y) (_ : x * y )) {x : M} (h : ) :
p x h
theorem AddSubmonoid.induction_of_closure_eq_top_left {M : Type u_1} [] {s : Set M} {p : MProp} (hs : ) (x : M) (H1 : p 0) (Hmul : xs, ∀ (y : M), p yp (x + y)) :
p x
theorem Submonoid.induction_of_closure_eq_top_left {M : Type u_1} [] {s : Set M} {p : MProp} (hs : ) (x : M) (H1 : p 1) (Hmul : xs, ∀ (y : M), p yp (x * y)) :
p x
theorem AddSubmonoid.closure_induction_right {M : Type u_1} [] {s : Set M} {p : (m : M) → } (one : p 0 (_ : )) (mul_right : ∀ (x : M) (hx : ) (y : M) (hy : y s), p x hxp (x + y) (_ : x + y )) {x : M} (h : ) :
p x h
theorem Submonoid.closure_induction_right {M : Type u_1} [] {s : Set M} {p : (m : M) → Prop} (one : p 1 (_ : )) (mul_right : ∀ (x : M) (hx : ) (y : M) (hy : y s), p x hxp (x * y) (_ : x * y )) {x : M} (h : ) :
p x h
theorem AddSubmonoid.induction_of_closure_eq_top_right {M : Type u_1} [] {s : Set M} {p : MProp} (hs : ) (x : M) (H1 : p 0) (Hmul : ∀ (x y : M), y sp xp (x + y)) :
p x
theorem Submonoid.induction_of_closure_eq_top_right {M : Type u_1} [] {s : Set M} {p : MProp} (hs : ) (x : M) (H1 : p 1) (Hmul : ∀ (x y : M), y sp xp (x * y)) :
p x
def Submonoid.powers {M : Type u_1} [] (n : M) :

The submonoid generated by an element.

Equations
Instances For
@[simp]
theorem Submonoid.mem_powers {M : Type u_1} [] (n : M) :
theorem Submonoid.coe_powers {M : Type u_1} [] (x : M) :
() = Set.range fun (n : ) => x ^ n
theorem Submonoid.mem_powers_iff {M : Type u_1} [] (x : M) (z : M) :
∃ (n : ), z ^ n = x
noncomputable instance Submonoid.decidableMemPowers {M : Type u_1} [] {a : M} :
DecidablePred fun (x : M) =>
Equations
noncomputable instance Submonoid.fintypePowers {M : Type u_1} [] {a : M} [] :
Equations
• Submonoid.fintypePowers =
theorem Submonoid.powers_eq_closure {M : Type u_1} [] (n : M) :
theorem Submonoid.powers_le {M : Type u_1} [] {n : M} {P : } :
n P
@[simp]
theorem Submonoid.powers_one {M : Type u_1} [] :
@[inline, reducible]
abbrev Submonoid.groupPowers {M : Type u_1} [] {x : M} {n : } (hpos : 0 < n) (hx : x ^ n = 1) :

The submonoid generated by an element is a group if that element has finite order.

Equations
Instances For
@[simp]
theorem Submonoid.pow_coe {M : Type u_1} [] (n : M) (m : ) :
() = n ^ m
def Submonoid.pow {M : Type u_1} [] (n : M) (m : ) :
()

Exponentiation map from natural numbers to powers.

Equations
• = () (Multiplicative.ofAdd m)
Instances For
theorem Submonoid.pow_apply {M : Type u_1} [] (n : M) (m : ) :
= { val := n ^ m, property := (_ : ∃ (y : ), (fun (x : ) => n ^ x) y = n ^ m) }
def Submonoid.log {M : Type u_1} [] [] {n : M} (p : ()) :

Logarithms from powers to natural numbers.

Equations
Instances For
@[simp]
theorem Submonoid.pow_log_eq_self {M : Type u_1} [] [] {n : M} (p : ()) :
= p
theorem Submonoid.pow_right_injective_iff_pow_injective {M : Type u_1} [] {n : M} :
(Function.Injective fun (m : ) => n ^ m)
@[simp]
theorem Submonoid.log_pow_eq_self {M : Type u_1} [] [] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (m : ) :
= m
@[simp]
theorem Submonoid.powLogEquiv_apply {M : Type u_1} [] [] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (m : ) :
= Submonoid.pow n (Multiplicative.toAdd m)
@[simp]
theorem Submonoid.powLogEquiv_symm_apply {M : Type u_1} [] [] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (m : ()) :
def Submonoid.powLogEquiv {M : Type u_1} [] [] {n : M} (h : Function.Injective fun (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
• One or more equations did not get rendered due to their size.
Instances For
theorem Submonoid.log_mul {M : Type u_1} [] [] {n : M} (h : Function.Injective fun (m : ) => n ^ m) (x : ()) (y : ()) :
theorem Submonoid.log_pow_int_eq_self {x : } (h : 1 < ) (m : ) :
= m
@[simp]
theorem Submonoid.map_powers {M : Type u_1} [] {N : Type u_4} {F : Type u_5} [] [FunLike F M N] [] (f : F) (m : M) :
def AddSubmonoid.closureAddCommMonoidOfComm {M : Type u_1} [] {s : Set M} (hcomm : as, bs, a + b = b + a) :

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

Equations
Instances For
theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_1 {M : Type u_1} [] {s : Set M} (hcomm : as, bs, a + b = b + a) (x : ) (y : ) :
x + y = y + x
def Submonoid.closureCommMonoidOfComm {M : Type u_1} [] {s : Set M} (hcomm : as, bs, a * b = b * a) :

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

Equations
Instances For
theorem VAddAssocClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [] [] [VAdd N α] [] {s : Set M} (htop : ) (hs : xs, ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)) :
theorem IsScalarTower.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [] [] [SMul N α] [] {s : Set M} (htop : ) (hs : xs, ∀ (y : N) (z : α), (x y) z = x y z) :
theorem VAddCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [] [VAdd N α] [] {s : Set M} (htop : ) (hs : xs, ∀ (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)) :
theorem SMulCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [] [SMul N α] [] {s : Set M} (htop : ) (hs : xs, ∀ (y : N) (z : α), x y z = y x z) :
theorem AddSubmonoid.sup_eq_range {N : Type u_4} [] (s : ) (t : ) :
theorem Submonoid.sup_eq_range {N : Type u_4} [] (s : ) (t : ) :
s t =
theorem AddSubmonoid.mem_sup {N : Type u_4} [] {s : } {t : } {x : N} :
x s t ∃ y ∈ s, ∃ z ∈ t, y + z = x
theorem Submonoid.mem_sup {N : Type u_4} [] {s : } {t : } {x : N} :
x s t ∃ y ∈ s, ∃ z ∈ t, y * z = x
theorem AddSubmonoid.mem_closure_singleton {A : Type u_2} [] {x : A} {y : A} :
∃ (n : ), n x = y

The AddSubmonoid generated by an element of an AddMonoid equals the set of natural number multiples of the element.

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

The additive submonoid generated by an element.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddSubmonoid.mem_multiples {M : Type u_1} [] (n : M) :
theorem AddSubmonoid.coe_multiples {M : Type u_1} [] (x : M) :
= Set.range fun (n : ) => n x
theorem AddSubmonoid.mem_multiples_iff {M : Type u_1} [] (x : M) (z : M) :
∃ (n : ), n z = x
noncomputable instance AddSubmonoid.decidableMemMultiples {M : Type u_1} [] {a : M} :
DecidablePred fun (x : M) =>
Equations
noncomputable instance AddSubmonoid.fintypeMultiples {M : Type u_1} [] {a : M} [] :
Equations
theorem AddSubmonoid.multiples_eq_closure {M : Type u_1} [] (n : M) :
theorem AddSubmonoid.multiples_le {M : Type u_1} [] {n : M} {P : } :
n P
@[simp]
theorem AddSubmonoid.multiples_zero {M : Type u_1} [] :
theorem AddSubmonoid.addGroupMultiples.proof_4 {M : Type u_1} [] {x : M} {n : } (hx : n x✝ = 0) (m : ) (x : ) :
(fun (z : ) (x : ) => Int.natMod z n x) () x = x + (fun (z : ) (x : ) => Int.natMod z n x) () x
theorem AddSubmonoid.addGroupMultiples.proof_5 {M : Type u_1} [] {x : M} {n : } (hpos : 0 < n) (hx : n x✝ = 0) (m : ) (x : ) :
(fun (z : ) (x : ) => Int.natMod z n x) () x = -(fun (z : ) (x : ) => Int.natMod z n x) (()) x
theorem AddSubmonoid.addGroupMultiples.proof_2 {M : Type u_1} [] {x : M} {n : } :
∀ (a b : ), a - b = a - b
abbrev AddSubmonoid.addGroupMultiples {M : Type u_1} [] {x : M} {n : } (hpos : 0 < n) (hx : n x = 0) :

The additive submonoid generated by an element is an additive group if that element has finite order.

Equations
Instances For
theorem AddSubmonoid.addGroupMultiples.proof_3 {M : Type u_1} [] {x : M} {n : } (z : ) :
Int.toNat (0 % n) z = 0
theorem AddSubmonoid.addGroupMultiples.proof_6 {M : Type u_1} [] {x : M} {n : } (hpos : 0 < n) (hx : n x = 0) (y : ) :
-y + y = 0

Lemmas about additive closures of Subsemigroup.

theorem MulMemClass.mul_right_mem_add_closure {M : Type u_1} {R : Type u_4} [SetLike M R] [] {S : M} {a : R} {b : R} (ha : ) (hb : b S) :
a * b

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 MulMemClass.mul_mem_add_closure {M : Type u_1} {R : Type u_4} [SetLike M R] [] {S : M} {a : R} {b : R} (ha : ) (hb : ) :
a * b

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

theorem MulMemClass.mul_left_mem_add_closure {M : Type u_1} {R : Type u_4} [SetLike M R] [] {S : M} {a : R} {b : R} (ha : a S) (hb : ) :
a * b

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 AddSubmonoid.mem_closure_pair {A : Type u_4} [] (a : A) (b : A) (c : A) :
c AddSubmonoid.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_4} [] (a : A) (b : A) (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.

theorem ofMul_image_powers_eq_multiples_ofMul {M : Type u_1} [] {x : M} :