Unbundled submonoids (deprecated)

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines unbundled multiplicative and additive submonoids. Instead of using this file, please use Submonoid G and AddSubmonoid A, defined in GroupTheory.Submonoid.Basic.

Main definitions

IsAddSubmonoid (S : Set M) : the predicate that S is the underlying subset of an additive submonoid of M. The bundled variant AddSubmonoid M should be used in preference to this.

IsSubmonoid (S : Set M) : the predicate that S is the underlying subset of a submonoid of M. The bundled variant Submonoid M should be used in preference to this.

Tags

Submonoid, Submonoids, IsSubmonoid

structure IsAddSubmonoid {A : Type u_2} [AddMonoid A] (s : Set A) : Prop

s is an additive submonoid: a set containing 0 and closed under addition. Note that this structure is deprecated, and the bundled variant AddSubmonoid A should be preferred.

• zero_mem : 0 ∈ s✝

  The proposition that s contains 0.

• add_mem : ∀ {a b : A}, a ∈ s✝ → b ∈ s✝ → a + b ∈ s✝

  The proposition that s is closed under addition.

structure IsSubmonoid {M : Type u_1} [Monoid M] (s : Set M) : Prop

s is a submonoid: a set containing 1 and closed under multiplication. Note that this structure is deprecated, and the bundled variant Submonoid M should be preferred.

• one_mem : 1 ∈ s✝

  The proposition that s contains 1.

• mul_mem : ∀ {a b : M}, a ∈ s✝ → b ∈ s✝ → a * b ∈ s✝

  The proposition that s is closed under multiplication.

theorem Additive.isAddSubmonoid {M : Type u_1} [Monoid M] {s : Set M} : IsSubmonoid s → IsAddSubmonoid s

theorem Additive.isAddSubmonoid_iff {M : Type u_1} [Monoid M] {s : Set M} : IsAddSubmonoid s ↔ IsSubmonoid s

theorem Multiplicative.isSubmonoid {A : Type u_2} [AddMonoid A] {s : Set A} : IsAddSubmonoid s → IsSubmonoid s

theorem Multiplicative.isSubmonoid_iff {A : Type u_2} [AddMonoid A] {s : Set A} : IsSubmonoid s ↔ IsAddSubmonoid s

theorem IsAddSubmonoid.inter {M : Type u_1} [AddMonoid M] {s₁ : Set M} {s₂ : Set M} (is₁ : IsAddSubmonoid s₁) (is₂ : IsAddSubmonoid s₂) : IsAddSubmonoid (s₁ ∩ s₂)

The intersection of two AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

theorem IsSubmonoid.inter {M : Type u_1} [Monoid M] {s₁ : Set M} {s₂ : Set M} (is₁ : IsSubmonoid s₁) (is₂ : IsSubmonoid s₂) : IsSubmonoid (s₁ ∩ s₂)

The intersection of two submonoids of a monoid M is a submonoid of M.

theorem IsAddSubmonoid.iInter {M : Type u_1} [AddMonoid M] {ι : Sort u_3} {s : ι → Set M} (h : ∀ (y : ι), IsAddSubmonoid (s y)) : IsAddSubmonoid (Set.iInter s)

The intersection of an indexed set of AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

theorem IsSubmonoid.iInter {M : Type u_1} [Monoid M] {ι : Sort u_3} {s : ι → Set M} (h : ∀ (y : ι), IsSubmonoid (s y)) : IsSubmonoid (Set.iInter s)

The intersection of an indexed set of submonoids of a monoid M is a submonoid of M.

abbrev isAddSubmonoid_iUnion_of_directed.match_3 {M : Type u_2} {ι : Type u_1} {s : ι → Set M} : ∀ {b : M} (motive : (∃ (i : ι), b ∈ s i) → Prop) (x : ∃ (i : ι), b ∈ s i), (∀ (j : ι) (hj : b ∈ s j), motive (_ : ∃ (i : ι), b ∈ s i)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

abbrev isAddSubmonoid_iUnion_of_directed.match_2 {M : Type u_2} {ι : Type u_1} {s : ι → Set M} (i : ι) (j : ι) (motive : (∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) → Prop) : ∀ (x : ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k), (∀ (k : ι) (hk : s i ⊆ s k ∧ s j ⊆ s k), motive (_ : ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

abbrev isAddSubmonoid_iUnion_of_directed.match_1 {ι : Type u_1} (motive : Nonempty ι → Prop) : ∀ (hι : Nonempty ι), (∀ (i : ι), motive (_ : Nonempty ι)) → motive hι

Equations

• (_ : motive hι) = (_ : motive hι)

theorem isAddSubmonoid_iUnion_of_directed {M : Type u_1} [AddMonoid M] {ι : Type u_3} [hι : Nonempty ι] {s : ι → Set M} (hs : ∀ (i : ι), IsAddSubmonoid (s i)) (Directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) : IsAddSubmonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

theorem isSubmonoid_iUnion_of_directed {M : Type u_1} [Monoid M] {ι : Type u_3} [hι : Nonempty ι] {s : ι → Set M} (hs : ∀ (i : ι), IsSubmonoid (s i)) (Directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) : IsSubmonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of submonoids of a monoid M is a submonoid of M.

def multiples {M : Type u_1} [AddMonoid M] (x : M) : Set M

The set of natural number multiples 0, x, 2x, ... of an element x of an AddMonoid.

Equations

• multiples x = {y : M | ∃ (n : ℕ), n • x = y}

def powers {M : Type u_1} [Monoid M] (x : M) : Set M

The set of natural number powers 1, x, x², ... of an element x of a monoid.

Equations

• powers x = {y : M | ∃ (n : ℕ), x ^ n = y}

theorem multiples.zero_mem {M : Type u_1} [AddMonoid M] {x : M} : 0 ∈ multiples x

0 is in the set of natural number multiples of an element of an AddMonoid.

theorem powers.one_mem {M : Type u_1} [Monoid M] {x : M} : 1 ∈ powers x

1 is in the set of natural number powers of an element of a monoid.

theorem multiples.self_mem {M : Type u_1} [AddMonoid M] {x : M} : x ∈ multiples x

An element of an AddMonoid is in the set of that element's natural number multiples.

theorem powers.self_mem {M : Type u_1} [Monoid M] {x : M} : x ∈ powers x

An element of a monoid is in the set of that element's natural number powers.

theorem multiples.add_mem {M : Type u_1} [AddMonoid M] {x : M} {y : M} {z : M} : y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x

The set of natural number multiples of an element of an AddMonoid is closed under addition.

abbrev multiples.add_mem.match_1 {M : Type u_1} [AddMonoid M] {x : M} {z : M} (motive : z ∈ multiples x → Prop) : ∀ (x_1 : z ∈ multiples x), (∀ (n₂ : ℕ) (h₂ : n₂ • x = z), motive (_ : ∃ (n : ℕ), n • x = z)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem powers.mul_mem {M : Type u_1} [Monoid M] {x : M} {y : M} {z : M} : y ∈ powers x → z ∈ powers x → y * z ∈ powers x

The set of natural number powers of an element of a monoid is closed under multiplication.

theorem multiples.isAddSubmonoid {M : Type u_1} [AddMonoid M] (x : M) : IsAddSubmonoid (multiples x)

The set of natural number multiples of an element of an AddMonoid M is an AddSubmonoid of M.

theorem powers.isSubmonoid {M : Type u_1} [Monoid M] (x : M) : IsSubmonoid (powers x)

The set of natural number powers of an element of a monoid M is a submonoid of M.

theorem Univ.isAddSubmonoid {M : Type u_1} [AddMonoid M] : IsAddSubmonoid Set.univ

An AddMonoid is an AddSubmonoid of itself.

theorem Univ.isSubmonoid {M : Type u_1} [Monoid M] : IsSubmonoid Set.univ

A monoid is a submonoid of itself.

theorem IsAddSubmonoid.preimage {M : Type u_1} [AddMonoid M] {N : Type u_3} [AddMonoid N] {f : M → N} (hf : IsAddMonoidHom f) {s : Set N} (hs : IsAddSubmonoid s) : IsAddSubmonoid (f ⁻¹' s)

The preimage of an AddSubmonoid under an AddMonoid hom is an AddSubmonoid of the domain.

theorem IsSubmonoid.preimage {M : Type u_1} [Monoid M] {N : Type u_3} [Monoid N] {f : M → N} (hf : IsMonoidHom f) {s : Set N} (hs : IsSubmonoid s) : IsSubmonoid (f ⁻¹' s)

The preimage of a submonoid under a monoid hom is a submonoid of the domain.

theorem IsAddSubmonoid.image {M : Type u_1} [AddMonoid M] {γ : Type u_3} [AddMonoid γ] {f : M → γ} (hf : IsAddMonoidHom f) {s : Set M} (hs : IsAddSubmonoid s) : IsAddSubmonoid (f '' s)

The image of an AddSubmonoid under an AddMonoid hom is an AddSubmonoid of the codomain.

abbrev IsAddSubmonoid.image.match_1 {M : Type u_2} {γ : Type u_1} {f : M → γ} {s : Set M} (b : γ) (motive : b ∈ f '' s → Prop) : ∀ (x : b ∈ f '' s), (∀ (y : M) (hy : y ∈ s ∧ f y = b), motive (_ : ∃ a ∈ s, f a = b)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem IsSubmonoid.image {M : Type u_1} [Monoid M] {γ : Type u_3} [Monoid γ] {f : M → γ} (hf : IsMonoidHom f) {s : Set M} (hs : IsSubmonoid s) : IsSubmonoid (f '' s)

The image of a submonoid under a monoid hom is a submonoid of the codomain.

theorem Range.isAddSubmonoid {M : Type u_1} [AddMonoid M] {γ : Type u_3} [AddMonoid γ] {f : M → γ} (hf : IsAddMonoidHom f) : IsAddSubmonoid (Set.range f)

The image of an AddMonoid hom is an AddSubmonoid of the codomain.

theorem Range.isSubmonoid {M : Type u_1} [Monoid M] {γ : Type u_3} [Monoid γ] {f : M → γ} (hf : IsMonoidHom f) : IsSubmonoid (Set.range f)

The image of a monoid hom is a submonoid of the codomain.

theorem IsAddSubmonoid.nsmul_mem {M : Type u_1} [AddMonoid M] {s : Set M} {a : M} (hs : IsAddSubmonoid s) (h : a ∈ s) {n : ℕ} : n • a ∈ s

An AddSubmonoid is closed under multiplication by naturals.

abbrev IsAddSubmonoid.nsmul_mem.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive (Nat.succ n)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem IsSubmonoid.pow_mem {M : Type u_1} [Monoid M] {s : Set M} {a : M} (hs : IsSubmonoid s) (h : a ∈ s) {n : ℕ} : a ^ n ∈ s

Submonoids are closed under natural powers.

theorem IsAddSubmonoid.multiples_subset {M : Type u_1} [AddMonoid M] {s : Set M} {a : M} (hs : IsAddSubmonoid s) (h : a ∈ s) : multiples a ⊆ s

The set of natural number multiples of an element of an AddSubmonoid is a subset of the AddSubmonoid.

theorem IsSubmonoid.power_subset {M : Type u_1} [Monoid M] {s : Set M} {a : M} (hs : IsSubmonoid s) (h : a ∈ s) : powers a ⊆ s

The set of natural number powers of an element of a submonoid is a subset of the submonoid.

abbrev IsAddSubmonoid.list_sum_mem.match_1 {M : Type u_1} {s : Set M} (motive : (x : List M) → (∀ x_1 ∈ x, x_1 ∈ s) → Prop) : ∀ (x : List M) (x_1 : ∀ x_1 ∈ x, x_1 ∈ s), (∀ (x : ∀ x ∈ [], x ∈ s), motive [] x) → (∀ (a : M) (l : List M) (h : ∀ x ∈ a :: l, x ∈ s), motive (a :: l) h) → motive x x_1

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

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

The sum of a list of elements of an AddSubmonoid is an element of the AddSubmonoid.

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

The product of a list of elements of a submonoid is an element of the submonoid.

theorem IsAddSubmonoid.multiset_sum_mem {M : Type u_3} [AddCommMonoid M] {s : Set M} (hs : IsAddSubmonoid s) (m : Multiset M) : (∀ a ∈ m, a ∈ s) → Multiset.sum m ∈ s

The sum of a multiset of elements of an AddSubmonoid of an AddCommMonoid is an element of the AddSubmonoid.

theorem IsSubmonoid.multiset_prod_mem {M : Type u_3} [CommMonoid M] {s : Set M} (hs : IsSubmonoid s) (m : Multiset M) : (∀ a ∈ m, a ∈ s) → Multiset.prod m ∈ s

The product of a multiset of elements of a submonoid of a CommMonoid is an element of the submonoid.

abbrev IsAddSubmonoid.finset_sum_mem.match_1 {M : Type u_2} {A : Type u_1} {s : Set M} (f : A → M) (motive : (x : Finset A) → (∀ b ∈ x, f b ∈ s) → Prop) : ∀ (x : Finset A) (x_1 : ∀ b ∈ x, f b ∈ s), (∀ (m : Multiset A) (hm : Multiset.Nodup m) (x : ∀ b ∈ { val := m, nodup := hm }, f b ∈ s), motive { val := m, nodup := hm } x) → motive x x_1

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

theorem IsAddSubmonoid.finset_sum_mem {M : Type u_3} {A : Type u_4} [AddCommMonoid M] {s : Set M} (hs : IsAddSubmonoid s) (f : A → M) (t : Finset A) : (∀ b ∈ t, f b ∈ s) → (Finset.sum t fun (b : A) => f b) ∈ s

The sum of elements of an AddSubmonoid of an AddCommMonoid indexed by a Finset is an element of the AddSubmonoid.

theorem IsSubmonoid.finset_prod_mem {M : Type u_3} {A : Type u_4} [CommMonoid M] {s : Set M} (hs : IsSubmonoid s) (f : A → M) (t : Finset A) : (∀ b ∈ t, f b ∈ s) → (Finset.prod t fun (b : A) => f b) ∈ s

The product of elements of a submonoid of a CommMonoid indexed by a Finset is an element of the submonoid.

inductive AddMonoid.InClosure {A : Type u_2} [AddMonoid A] (s : Set A) : A → Prop

The inductively defined membership predicate for the submonoid generated by a subset of a monoid.

• basic: ∀ {A : Type u_2} [inst : AddMonoid A] {s : Set A} {a : A}, a ∈ s → AddMonoid.InClosure s a
• zero: ∀ {A : Type u_2} [inst : AddMonoid A] {s : Set A}, AddMonoid.InClosure s 0
• add: ∀ {A : Type u_2} [inst : AddMonoid A] {s : Set A} {a b : A}, AddMonoid.InClosure s a → AddMonoid.InClosure s b → AddMonoid.InClosure s (a + b)

inductive Monoid.InClosure {M : Type u_1} [Monoid M] (s : Set M) : M → Prop

The inductively defined membership predicate for the Submonoid generated by a subset of an monoid.

• basic: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M}, a ∈ s → Monoid.InClosure s a
• one: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, Monoid.InClosure s 1
• mul: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a b : M}, Monoid.InClosure s a → Monoid.InClosure s b → Monoid.InClosure s (a * b)

def AddMonoid.Closure {M : Type u_1} [AddMonoid M] (s : Set M) : Set M

The inductively defined AddSubmonoid generated by a subset of an AddMonoid.

Equations

• AddMonoid.Closure s = {a : M | AddMonoid.InClosure s a}

def Monoid.Closure {M : Type u_1} [Monoid M] (s : Set M) : Set M

The inductively defined submonoid generated by a subset of a monoid.

Equations

• Monoid.Closure s = {a : M | Monoid.InClosure s a}

theorem AddMonoid.closure.isAddSubmonoid {M : Type u_1} [AddMonoid M] (s : Set M) : IsAddSubmonoid (AddMonoid.Closure s)

theorem Monoid.closure.isSubmonoid {M : Type u_1} [Monoid M] (s : Set M) : IsSubmonoid (Monoid.Closure s)

theorem AddMonoid.subset_closure {M : Type u_1} [AddMonoid M] {s : Set M} : s ⊆ AddMonoid.Closure s

A subset of an AddMonoid is contained in the AddSubmonoid it generates.

theorem Monoid.subset_closure {M : Type u_1} [Monoid M] {s : Set M} : s ⊆ Monoid.Closure s

A subset of a monoid is contained in the submonoid it generates.

theorem AddMonoid.closure_subset {M : Type u_1} [AddMonoid M] {s : Set M} {t : Set M} (ht : IsAddSubmonoid t) (h : s ⊆ t) : AddMonoid.Closure s ⊆ t

The AddSubmonoid generated by a set is contained in any AddSubmonoid that contains the set.

theorem Monoid.closure_subset {M : Type u_1} [Monoid M] {s : Set M} {t : Set M} (ht : IsSubmonoid t) (h : s ⊆ t) : Monoid.Closure s ⊆ t

The submonoid generated by a set is contained in any submonoid that contains the set.

theorem AddMonoid.closure_mono {M : Type u_1} [AddMonoid M] {s : Set M} {t : Set M} (h : s ⊆ t) : AddMonoid.Closure s ⊆ AddMonoid.Closure t

Given subsets t and s of an AddMonoid M, if s ⊆ t, the AddSubmonoid of M generated by s is contained in the AddSubmonoid generated by t.

theorem Monoid.closure_mono {M : Type u_1} [Monoid M] {s : Set M} {t : Set M} (h : s ⊆ t) : Monoid.Closure s ⊆ Monoid.Closure t

Given subsets t and s of a monoid M, if s ⊆ t, the submonoid of M generated by s is contained in the submonoid generated by t.

theorem AddMonoid.closure_singleton {M : Type u_1} [AddMonoid M] {x : M} : AddMonoid.Closure {x} = multiples x

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

theorem Monoid.closure_singleton {M : Type u_1} [Monoid M] {x : M} : Monoid.Closure {x} = powers x

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

theorem AddMonoid.image_closure {M : Type u_1} [AddMonoid M] {A : Type u_3} [AddMonoid A] {f : M → A} (hf : IsAddMonoidHom f) (s : Set M) : f '' AddMonoid.Closure s = AddMonoid.Closure (f '' s)

The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set under the AddMonoid hom.

theorem Monoid.image_closure {M : Type u_1} [Monoid M] {A : Type u_3} [Monoid A] {f : M → A} (hf : IsMonoidHom f) (s : Set M) : f '' Monoid.Closure s = Monoid.Closure (f '' s)

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set under the monoid hom.

theorem AddMonoid.exists_list_of_mem_closure {M : Type u_1} [AddMonoid M] {s : Set M} {a : M} (h : a ∈ AddMonoid.Closure s) : ∃ (l : List M), (∀ x ∈ l, x ∈ s) ∧ List.sum l = a

Given an element a of the AddSubmonoid of an AddMonoid M generated by a set s, there exists a list of elements of s whose sum is a.

theorem Monoid.exists_list_of_mem_closure {M : Type u_1} [Monoid M] {s : Set M} {a : M} (h : a ∈ Monoid.Closure s) : ∃ (l : List M), (∀ x ∈ l, x ∈ s) ∧ List.prod l = a

Given an element a of the submonoid of a monoid M generated by a set s, there exists a list of elements of s whose product is a.

abbrev AddMonoid.mem_closure_union_iff.match_3 {M : Type u_1} [AddCommMonoid M] {s : Set M} {t : Set M} {x : M} (motive : (∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x) → Prop) : ∀ (x_1 : ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x), (∀ (y : M) (hy : y ∈ AddMonoid.Closure s) (z : M) (hz : z ∈ AddMonoid.Closure t) (hyzx : y + z = x), motive (_ : ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem AddMonoid.mem_closure_union_iff {M : Type u_3} [AddCommMonoid M] {s : Set M} {t : Set M} {x : M} : x ∈ AddMonoid.Closure (s ∪ t) ↔ ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x

Given sets s, t of a commutative AddMonoid M, x ∈ M is in the AddSubmonoid of M generated by s ∪ t iff there exists an element of the AddSubmonoid generated by s and an element of the AddSubmonoid generated by t whose sum is x.

abbrev AddMonoid.mem_closure_union_iff.match_1 {M : Type u_1} [AddCommMonoid M] {s : Set M} {t : Set M} (tl : List M) (motive : (∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = List.sum tl) → Prop) : ∀ (x : ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = List.sum tl), (∀ (y : M) (hy : y ∈ AddMonoid.Closure s) (z : M) (hz : z ∈ AddMonoid.Closure t) (hyzx : y + z = List.sum tl), motive (_ : ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = List.sum tl)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

abbrev AddMonoid.mem_closure_union_iff.match_2 {M : Type u_1} [AddCommMonoid M] {s : Set M} {t : Set M} {x : M} (motive : (∃ (l : List M), (∀ x ∈ l, x ∈ s ∪ t) ∧ List.sum l = x) → Prop) : ∀ (x_1 : ∃ (l : List M), (∀ x ∈ l, x ∈ s ∪ t) ∧ List.sum l = x), (∀ (L : List M) (HL1 : ∀ x ∈ L, x ∈ s ∪ t) (HL2 : List.sum L = x), motive (_ : ∃ (l : List M), (∀ x ∈ l, x ∈ s ∪ t) ∧ List.sum l = x)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem Monoid.mem_closure_union_iff {M : Type u_3} [CommMonoid M] {s : Set M} {t : Set M} {x : M} : x ∈ Monoid.Closure (s ∪ t) ↔ ∃ y ∈ Monoid.Closure s, ∃ z ∈ Monoid.Closure t, y * z = x

Given sets s, t of a commutative monoid M, x ∈ M is in the submonoid of M generated by s ∪ t iff there exists an element of the submonoid generated by s and an element of the submonoid generated by t whose product is x.

def AddSubmonoid.of {M : Type u_1} [AddMonoid M] {s : Set M} (h : IsAddSubmonoid s) : AddSubmonoid M

Create a bundled additive submonoid from a set s and [IsAddSubmonoid s].

Equations

• AddSubmonoid.of h = { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ (x x_1 : M), x ∈ s → x_1 ∈ s → x + x_1 ∈ s) }, zero_mem' := (_ : 0 ∈ s) }

def Submonoid.of {M : Type u_1} [Monoid M] {s : Set M} (h : IsSubmonoid s) : Submonoid M

Create a bundled submonoid from a set s and [IsSubmonoid s].

Equations

• Submonoid.of h = { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ (x x_1 : M), x ∈ s → x_1 ∈ s → x * x_1 ∈ s) }, one_mem' := (_ : 1 ∈ s) }

theorem AddSubmonoid.isAddSubmonoid {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : IsAddSubmonoid ↑S

theorem Submonoid.isSubmonoid {M : Type u_1} [Monoid M] (S : Submonoid M) : IsSubmonoid ↑S