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} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} (l : List { x // x ∈ S }) : ↑(List.sum l) = List.sum (List.map Subtype.val l)

@[simp]

theorem SubmonoidClass.coe_list_prod {M : Type u_1} {B : Type u_3} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} (l : List { x // x ∈ S }) : ↑(List.prod l) = List.prod (List.map Subtype.val l)

@[simp]

theorem AddSubmonoidClass.coe_multiset_sum {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset { x // x ∈ S }) : ↑(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)

@[simp]

theorem SubmonoidClass.coe_multiset_prod {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset { x // x ∈ S }) : ↑(Multiset.prod m) = 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} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (f : ι → { x // x ∈ S }) (s : Finset ι) : ↑(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} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ι → { x // x ∈ S }) (s : Finset ι) : ↑(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} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} {l : List M} (hl : ∀ (x : M), x ∈ l → x ∈ S) : List.sum l ∈ 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} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} {l : List M} (hl : ∀ (x : M), x ∈ l → x ∈ S) : List.prod l ∈ 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} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) : Multiset.sum m ∈ 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} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) : Multiset.prod m ∈ 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 : Finset ι} {f : ι → M} (_x : M) (motive : (∃ a, a ∈ t.val ∧ f a = _x) → Prop) : (x : ∃ a, a ∈ t.val ∧ f a = _x) → ((i : ι) → (hi : i ∈ t.val) → (hix : f i = _x) → motive (_ : ∃ a, a ∈ t.val ∧ f a = _x)) → motive x

Equations

• sum_mem.match_1 _x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem sum_mem {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → 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} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → 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} [AddMonoid M] (s : AddSubmonoid M) (l : List { x // x ∈ s }) : ↑(List.sum l) = List.sum (List.map Subtype.val l)

theorem Submonoid.coe_list_prod {M : Type u_1} [Monoid M] (s : Submonoid M) (l : List { x // x ∈ s }) : ↑(List.prod l) = List.prod (List.map Subtype.val l)

theorem AddSubmonoid.coe_multiset_sum {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset { x // x ∈ S }) : ↑(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)

theorem Submonoid.coe_multiset_prod {M : Type u_4} [CommMonoid M] (S : Submonoid M) (m : Multiset { x // x ∈ S }) : ↑(Multiset.prod m) = Multiset.prod (Multiset.map Subtype.val m)

@[simp]

theorem AddSubmonoid.coe_finset_sum {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] (S : AddSubmonoid M) (f : ι → { x // x ∈ S }) (s : Finset ι) : ↑(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} [CommMonoid M] (S : Submonoid M) (f : ι → { x // x ∈ S }) (s : Finset ι) : ↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)

theorem AddSubmonoid.list_sum_mem {M : Type u_1} [AddMonoid M] (s : AddSubmonoid M) {l : List M} (hl : ∀ (x : M), x ∈ l → x ∈ s) : List.sum l ∈ s

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

theorem Submonoid.list_prod_mem {M : Type u_1} [Monoid M] (s : Submonoid M) {l : List M} (hl : ∀ (x : M), x ∈ l → x ∈ s) : List.prod l ∈ s

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

theorem AddSubmonoid.multiset_sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) : Multiset.sum m ∈ 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} [CommMonoid M] (S : Submonoid M) (m : Multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) : Multiset.prod m ∈ 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} [AddMonoid M] (S : AddSubmonoid M) (m : Multiset M) (comm : Set.Pairwise {x | x ∈ m} AddCommute) (h : ∀ (x : M), x ∈ m → x ∈ S) : Multiset.noncommSum m comm ∈ S

theorem Submonoid.multiset_noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) (m : Multiset M) (comm : Set.Pairwise {x | x ∈ m} Commute) (h : ∀ (x : M), x ∈ m → x ∈ S) : Multiset.noncommProd m comm ∈ S

theorem AddSubmonoid.sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → 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} [CommMonoid M] (S : Submonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → 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} [AddMonoid M] (S : AddSubmonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : Set.Pairwise ↑t fun a b => AddCommute (f a) (f b)) (h : ∀ (c : ι), c ∈ t → f c ∈ S) : Finset.noncommSum t f comm ∈ S

theorem Submonoid.noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)) (h : ∀ (c : ι), c ∈ t → f c ∈ S) : Finset.noncommProd t f comm ∈ S

abbrev AddSubmonoid.mem_iSup_of_directed.match_1 {M : Type u_2} [AddZeroClass M] {ι : Sort u_1} {S : ι → AddSubmonoid M} {x : M} (motive : (∃ i, x ∈ S i) → Prop) : (x : ∃ i, x ∈ S i) → ((i : ι) → (hi : x ∈ S i) → motive (_ : ∃ i, x ∈ S i)) → motive x

Equations

• AddSubmonoid.mem_iSup_of_directed.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem AddSubmonoid.mem_iSup_of_directed {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} [hι : Nonempty ι] {S : ι → AddSubmonoid M} (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} [MulOneClass M] {ι : Sort u_4} [hι : Nonempty ι] {S : ι → Submonoid M} (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} [AddZeroClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → AddSubmonoid M} (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} [MulOneClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → Submonoid M} (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} [AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x ≤ x_1) S) {x : M} : x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s

theorem Submonoid.mem_sSup_of_directedOn {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x ≤ x_1) S) {x : M} : x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s

theorem AddSubmonoid.coe_sSup_of_directedOn {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x ≤ x_1) S) : ↑(sSup S) = ⋃ (s : AddSubmonoid M) (_ : s ∈ S), ↑s

theorem Submonoid.coe_sSup_of_directedOn {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x ≤ x_1) S) : ↑(sSup S) = ⋃ (s : Submonoid M) (_ : s ∈ S), ↑s

theorem AddSubmonoid.mem_sup_left {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem Submonoid.mem_sup_left {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem AddSubmonoid.mem_sup_right {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem Submonoid.mem_sup_right {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem AddSubmonoid.add_mem_sup {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} {x : M} {y : M} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Submonoid.mul_mem_sup {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} {x : M} {y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubmonoid.mem_iSup_of_mem {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem Submonoid.mem_iSup_of_mem {M : Type u_1} [MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem AddSubmonoid.mem_sSup_of_mem {M : Type u_1} [AddZeroClass M] {S : Set (AddSubmonoid M)} {s : AddSubmonoid M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem Submonoid.mem_sSup_of_mem {M : Type u_1} [MulOneClass M] {S : Set (Submonoid M)} {s : Submonoid M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem AddSubmonoid.iSup_induction {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid 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.iSup_induction {M : Type u_1} [MulOneClass M] {ι : Sort u_4} (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 AddSubmonoid.iSup_induction' {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (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 hx → C y hy → C (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} [MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (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 hx → C y hy → C (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 FreeAddMonoid.closure_range_of {α : Type u_4} : AddSubmonoid.closure (Set.range FreeAddMonoid.of) = ⊤

theorem FreeMonoid.closure_range_of {α : Type u_4} : Submonoid.closure (Set.range FreeMonoid.of) = ⊤

theorem Submonoid.closure_singleton_eq {M : Type u_1} [Monoid M] (x : M) : Submonoid.closure {x} = MonoidHom.mrange (↑(powersHom M) x)

theorem Submonoid.mem_closure_singleton {M : Type u_1} [Monoid M] {x : M} {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} : y ∈ Submonoid.closure {y}

theorem Submonoid.closure_singleton_one {M : Type u_1} [Monoid M] : Submonoid.closure {1} = ⊥

theorem FreeAddMonoid.mrange_lift {M : Type u_1} [AddMonoid M] {α : Type u_4} (f : α → M) : AddMonoidHom.mrange (↑FreeAddMonoid.lift f) = AddSubmonoid.closure (Set.range f)

theorem FreeMonoid.mrange_lift {M : Type u_1} [Monoid M] {α : Type u_4} (f : α → M) : MonoidHom.mrange (↑FreeMonoid.lift f) = Submonoid.closure (Set.range f)

theorem AddSubmonoid.closure_eq_mrange {M : Type u_1} [AddMonoid M] (s : Set M) : AddSubmonoid.closure s = AddMonoidHom.mrange (↑FreeAddMonoid.lift Subtype.val)

theorem Submonoid.closure_eq_mrange {M : Type u_1} [Monoid M] (s : Set M) : Submonoid.closure s = MonoidHom.mrange (↑FreeMonoid.lift Subtype.val)

theorem AddSubmonoid.closure_eq_image_sum {M : Type u_1} [AddMonoid M] (s : Set M) : ↑(AddSubmonoid.closure s) = List.sum '' {l | ∀ (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 | ∀ (x : M), x ∈ l → x ∈ s}

theorem AddSubmonoid.exists_list_of_mem_closure {M : Type u_1} [AddMonoid M] {s : Set M} {x : M} (hx : x ∈ AddSubmonoid.closure s) : ∃ l x, List.sum l = x

theorem Submonoid.exists_list_of_mem_closure {M : Type u_1} [Monoid M] {s : Set M} {x : M} (hx : x ∈ Submonoid.closure s) : ∃ l x, List.prod l = x

theorem AddSubmonoid.exists_multiset_of_mem_closure {M : Type u_4} [AddCommMonoid M] {s : Set M} {x : M} (hx : x ∈ AddSubmonoid.closure s) : ∃ l x, Multiset.sum l = x

theorem Submonoid.exists_multiset_of_mem_closure {M : Type u_4} [CommMonoid M] {s : Set M} {x : M} (hx : x ∈ Submonoid.closure s) : ∃ l x, Multiset.prod l = x

theorem AddSubmonoid.closure_induction_left {M : Type u_1} [AddMonoid M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ AddSubmonoid.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 AddSubmonoid.induction_of_closure_eq_top_left {M : Type u_1} [AddMonoid M] {s : Set M} {p : M → Prop} (hs : AddSubmonoid.closure s = ⊤) (x : M) (H1 : p 0) (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 AddSubmonoid.closure_induction_right {M : Type u_1} [AddMonoid M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ AddSubmonoid.closure s) (H1 : p 0) (Hmul : (x y : M) → y ∈ s → p x → 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 AddSubmonoid.induction_of_closure_eq_top_right {M : Type u_1} [AddMonoid M] {s : Set M} {p : M → Prop} (hs : AddSubmonoid.closure s = ⊤) (x : M) (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

def Submonoid.powers {M : Type u_1} [Monoid M] (n : M) : Submonoid M

The submonoid generated by an element.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submonoid.mem_powers {M : Type u_1} [Monoid M] (n : M) : n ∈ Submonoid.powers n

theorem Submonoid.coe_powers {M : Type u_1} [Monoid M] (x : M) : ↑(Submonoid.powers x) = Set.range fun n => x ^ n

theorem Submonoid.mem_powers_iff {M : Type u_1} [Monoid M] (x : M) (z : M) : x ∈ Submonoid.powers z ↔ ∃ n, z ^ n = x

theorem Submonoid.powers_eq_closure {M : Type u_1} [Monoid M] (n : M) : Submonoid.powers n = Submonoid.closure {n}

theorem Submonoid.powers_subset {M : Type u_1} [Monoid M] {n : M} {P : Submonoid M} (h : n ∈ P) : Submonoid.powers n ≤ P

@[simp]

theorem Submonoid.powers_one {M : Type u_1} [Monoid M] : Submonoid.powers 1 = ⊥

@[inline, reducible]

abbrev Submonoid.groupPowers {M : Type u_1} [Monoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group { x // x ∈ Submonoid.powers x }

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

Equations

• Submonoid.groupPowers hpos hx = Group.mk (_ : ∀ (y : { x // x ∈ Submonoid.powers x }), y⁻¹ * y = 1)

@[simp]

theorem Submonoid.pow_coe {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : ↑(Submonoid.pow n m) = n ^ m

def Submonoid.pow {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : { x // x ∈ Submonoid.powers n }

Exponentiation map from natural numbers to powers.

Equations

• Submonoid.pow n m = ↑(MonoidHom.mrangeRestrict (↑(powersHom M) n)) (↑Multiplicative.ofAdd m)

theorem Submonoid.pow_apply {M : Type u_1} [Monoid M] (n : M) (m : ℕ) : Submonoid.pow n m = { val := n ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) n y = n ^ m) }

def Submonoid.log {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : { x // x ∈ Submonoid.powers n }) : ℕ

Logarithms from powers to natural numbers.

Equations

• Submonoid.log p = Nat.find (_ : ∃ n, n ^ n = ↑p)

@[simp]

theorem Submonoid.pow_log_eq_self {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (p : { x // x ∈ 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 fun m => n ^ m) ↔ Function.Injective (Submonoid.pow n)

@[simp]

theorem Submonoid.log_pow_eq_self {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : ℕ) : Submonoid.log (Submonoid.pow n m) = m

@[simp]

theorem Submonoid.powLogEquiv_symm_apply {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : { x // x ∈ Submonoid.powers n }) : ↑(MulEquiv.symm (Submonoid.powLogEquiv h)) m = ↑Multiplicative.ofAdd (Submonoid.log m)

@[simp]

theorem Submonoid.powLogEquiv_apply {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (m : Multiplicative ℕ) : ↑(Submonoid.powLogEquiv h) m = Submonoid.pow n (↑Multiplicative.toAdd m)

def Submonoid.powLogEquiv {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) : Multiplicative ℕ ≃* { x // x ∈ Submonoid.powers n }

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.

theorem Submonoid.log_mul {M : Type u_1} [Monoid M] [DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m) (x : { x // x ∈ Submonoid.powers n }) (y : { x // x ∈ Submonoid.powers n }) : Submonoid.log (x * y) = Submonoid.log x + Submonoid.log y

theorem Submonoid.log_pow_int_eq_self {x : ℤ} (h : 1 < Int.natAbs x) (m : ℕ) : Submonoid.log (Submonoid.pow x m) = m

@[simp]

theorem Submonoid.map_powers {M : Type u_1} [Monoid M] {N : Type u_4} {F : Type u_5} [Monoid N] [MonoidHomClass F M N] (f : F) (m : M) : Submonoid.map f (Submonoid.powers m) = Submonoid.powers (↑f m)

theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_3 {M : Type u_1} [AddMonoid M] {s : Set M} (x : { x // x ∈ AddSubmonoid.closure s }) : AddMonoid.nsmul 0 x = 0

theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_5 {M : Type u_1} [AddMonoid M] {s : Set M} (hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a + b = b + a) (x : { x // x ∈ AddSubmonoid.closure s }) (y : { x // x ∈ AddSubmonoid.closure s }) : x + y = y + x

def AddSubmonoid.closureAddCommMonoidOfComm {M : Type u_1} [AddMonoid M] {s : Set M} (hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a + b = b + a) : AddCommMonoid { x // x ∈ AddSubmonoid.closure s }

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

Equations

• AddSubmonoid.closureAddCommMonoidOfComm hcomm = let src := AddSubmonoid.toAddMonoid (AddSubmonoid.closure s); AddCommMonoid.mk (_ : ∀ (x y : { x // x ∈ AddSubmonoid.closure s }), x + y = y + x)

theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_4 {M : Type u_1} [AddMonoid M] {s : Set M} (n : ℕ) (x : { x // x ∈ AddSubmonoid.closure s }) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_1 {M : Type u_1} [AddMonoid M] {s : Set M} (a : { x // x ∈ AddSubmonoid.closure s }) : 0 + a = a

theorem AddSubmonoid.closureAddCommMonoidOfComm.proof_2 {M : Type u_1} [AddMonoid M] {s : Set M} (a : { x // x ∈ AddSubmonoid.closure s }) : a + 0 = a

def Submonoid.closureCommMonoidOfComm {M : Type u_1} [Monoid M] {s : Set M} (hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a) : CommMonoid { x // x ∈ Submonoid.closure s }

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

Equations

• Submonoid.closureCommMonoidOfComm hcomm = let src := Submonoid.toMonoid (Submonoid.closure s); CommMonoid.mk (_ : ∀ (x y : { x // x ∈ Submonoid.closure s }), x * y = y * x)

theorem VAddAssocClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [AddMonoid M] [AddAction M N] [VAdd N α] [AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ⊤) (hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)) : VAddAssocClass M N α

theorem IsScalarTower.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [Monoid M] [MulAction M N] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤) (hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z) : IsScalarTower M N α

theorem VAddCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [AddMonoid M] [VAdd N α] [AddAction M α] {s : Set M} (htop : AddSubmonoid.closure s = ⊤) (hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)) : VAddCommClass M N α

theorem SMulCommClass.of_mclosure_eq_top {M : Type u_1} {N : Type u_4} {α : Type u_5} [Monoid M] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤) (hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z) : SMulCommClass M N α

theorem AddSubmonoid.sup_eq_range {N : Type u_4} [AddCommMonoid N] (s : AddSubmonoid N) (t : AddSubmonoid N) : s ⊔ t = AddMonoidHom.mrange (AddMonoidHom.coprod (AddSubmonoid.subtype s) (AddSubmonoid.subtype t))

theorem Submonoid.sup_eq_range {N : Type u_4} [CommMonoid N] (s : Submonoid N) (t : Submonoid N) : s ⊔ t = MonoidHom.mrange (MonoidHom.coprod (Submonoid.subtype s) (Submonoid.subtype t))

theorem AddSubmonoid.mem_sup {N : Type u_4} [AddCommMonoid N] {s : AddSubmonoid N} {t : AddSubmonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y + z = x

theorem Submonoid.mem_sup {N : Type u_4} [CommMonoid N] {s : Submonoid N} {t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x

theorem AddSubmonoid.closure_singleton_eq {A : Type u_2} [AddMonoid A] (x : A) : AddSubmonoid.closure {x} = AddMonoidHom.mrange (↑(multiplesHom A) x)

theorem AddSubmonoid.mem_closure_singleton {A : Type u_2} [AddMonoid A] {x : A} {y : A} : y ∈ AddSubmonoid.closure {x} ↔ ∃ n, n • x = y

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

theorem AddSubmonoid.closure_singleton_zero {A : Type u_2} [AddMonoid A] : AddSubmonoid.closure {0} = ⊥

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

The additive submonoid generated by an element.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubmonoid.mem_multiples {M : Type u_1} [AddMonoid M] (n : M) : n ∈ AddSubmonoid.multiples n

theorem AddSubmonoid.coe_multiples {M : Type u_1} [AddMonoid M] (x : M) : ↑(AddSubmonoid.multiples x) = Set.range fun n => n • x

theorem AddSubmonoid.mem_multiples_iff {M : Type u_1} [AddMonoid M] (x : M) (z : M) : x ∈ AddSubmonoid.multiples z ↔ ∃ n, n • z = x

theorem AddSubmonoid.multiples_eq_closure {M : Type u_1} [AddMonoid M] (n : M) : AddSubmonoid.multiples n = AddSubmonoid.closure {n}

abbrev AddSubmonoid.multiples_subset.match_1 {M : Type u_1} [AddMonoid M] {n : M} (motive : (x : M) → x ∈ AddSubmonoid.multiples n → Prop) : (x : M) → (hx : x ∈ AddSubmonoid.multiples n) → ((i : ℕ) → motive ((fun x x_1 => x_1 • x) n i) (_ : ∃ y, (fun x x_1 => x_1 • x) n y = (fun x x_1 => x_1 • x) n i)) → motive x hx

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.multiples_subset {M : Type u_1} [AddMonoid M] {n : M} {P : AddSubmonoid M} (h : n ∈ P) : AddSubmonoid.multiples n ≤ P

@[simp]

theorem AddSubmonoid.multiples_zero {M : Type u_1} [AddMonoid M] : AddSubmonoid.multiples 0 = ⊥

theorem AddSubmonoid.addGroupMultiples.proof_6 {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : n • x = 0) (y : { x // x ∈ AddSubmonoid.multiples x }) : -y + y = 0

theorem AddSubmonoid.addGroupMultiples.proof_4 {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (hx : n • x = 0) (m : ℕ) (x : { x // x ∈ AddSubmonoid.multiples x }) : (fun z x => Int.natMod z ↑n • x) (Int.ofNat (Nat.succ m)) x = x + (fun z x => Int.natMod z ↑n • x) (Int.ofNat m) x

theorem AddSubmonoid.addGroupMultiples.proof_5 {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : n • x = 0) (m : ℕ) (x : { x // x ∈ AddSubmonoid.multiples x }) : (fun z x => Int.natMod z ↑n • x) (Int.negSucc m) x = -(fun z x => Int.natMod z ↑n • x) (↑(Nat.succ m)) x

theorem AddSubmonoid.addGroupMultiples.proof_3 {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (z : { x // x ∈ AddSubmonoid.multiples x }) : Int.toNat (0 % ↑n) • z = 0

theorem AddSubmonoid.addGroupMultiples.proof_1 {M : Type u_1} [AddMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.addGroupMultiples.proof_2 {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} : ∀ (a b : { x // x ∈ AddSubmonoid.multiples x }), a - b = a - b

abbrev AddSubmonoid.addGroupMultiples {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : n • x = 0) : AddGroup { x // x ∈ AddSubmonoid.multiples x }

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

Equations

• AddSubmonoid.addGroupMultiples hpos hx = AddGroup.mk (_ : ∀ (y : { x // x ∈ AddSubmonoid.multiples x }), -y + y = 0)

Lemmas about additive closures of Subsemigroup.

theorem MulMemClass.mul_right_mem_add_closure {M : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M} {a : R} {b : R} (ha : a ∈ AddSubmonoid.closure ↑S) (hb : b ∈ S) : a * b ∈ AddSubmonoid.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 MulMemClass.mul_mem_add_closure {M : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M} {a : R} {b : R} (ha : a ∈ AddSubmonoid.closure ↑S) (hb : b ∈ AddSubmonoid.closure ↑S) : a * b ∈ AddSubmonoid.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 MulMemClass.mul_left_mem_add_closure {M : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M} {a : R} {b : R} (ha : a ∈ S) (hb : b ∈ AddSubmonoid.closure ↑S) : a * b ∈ AddSubmonoid.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 AddSubmonoid.mem_closure_pair {A : Type u_4} [AddCommMonoid A] (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} [CommMonoid A] (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} [Monoid M] {x : M} : ↑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (↑Additive.ofMul x))

theorem ofAdd_image_multiples_eq_powers_ofAdd {A : Type u_2} [AddMonoid A] {x : A} : ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (↑Multiplicative.ofAdd x))