# 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} [] (s : Set A) :

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 sb sa + b s

The proposition that s is closed under addition.

Instances For
theorem IsAddSubmonoid.zero_mem {A : Type u_2} [] {s : Set A} (self : ) :
0 s

The proposition that s contains 0.

theorem IsAddSubmonoid.add_mem {A : Type u_2} [] {s : Set A} (self : ) {a : A} {b : A} :
a sb sa + b s

The proposition that s is closed under addition.

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

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 sb sa * b s

The proposition that s is closed under multiplication.

Instances For
theorem IsSubmonoid.one_mem {M : Type u_1} [] {s : Set M} (self : ) :
1 s

The proposition that s contains 1.

theorem IsSubmonoid.mul_mem {M : Type u_1} [] {s : Set M} (self : ) {a : M} {b : M} :
a sb sa * b s

The proposition that s is closed under multiplication.

theorem Additive.isAddSubmonoid {M : Type u_1} [] {s : Set M} :
theorem Additive.isAddSubmonoid_iff {M : Type u_1} [] {s : Set M} :
theorem Multiplicative.isSubmonoid {A : Type u_2} [] {s : Set A} :
theorem Multiplicative.isSubmonoid_iff {A : Type u_2} [] {s : Set A} :
theorem IsAddSubmonoid.inter {M : Type u_1} [] {s₁ : Set M} {s₂ : Set M} (is₁ : ) (is₂ : ) :

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

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

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

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

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

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

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 )motive x
Equations
• =
Instances For
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 )motive x
Equations
• =
Instances For
abbrev isAddSubmonoid_iUnion_of_directed.match_1 {ι : Type u_1} (motive : Prop) :
∀ ( : ), (∀ (i : ι), motive )motive
Equations
• =
Instances For
theorem isAddSubmonoid_iUnion_of_directed {M : Type u_1} [] {ι : Type u_3} [hι : ] {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} [] {ι : Type u_3} [hι : ] {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} [] (x : M) :
Set M

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

Equations
Instances For
def powers {M : Type u_1} [] (x : M) :
Set M

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

Equations
• = {y : M | ∃ (n : ), x ^ n = y}
Instances For
theorem multiples.zero_mem {M : Type u_1} [] {x : M} :
0

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

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

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

theorem multiples.self_mem {M : Type u_1} [] {x : M} :
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} [] {x : M} :
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} [] {x : M} {y : M} {z : M} :
y z y + z

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} [] {x : M} {z : M} (motive : z Prop) :
∀ (x_1 : z ), (∀ (n₂ : ) (h₂ : n₂ x = z), motive )motive x_1
Equations
• =
Instances For
theorem powers.mul_mem {M : Type u_1} [] {x : M} {y : M} {z : M} :
y z y * z

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

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

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} [] (x : M) :

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} [] :

An AddMonoid is an AddSubmonoid of itself.

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

A monoid is a submonoid of itself.

theorem IsAddSubmonoid.preimage {M : Type u_1} [] {N : Type u_3} [] {f : MN} (hf : ) {s : Set N} (hs : ) :

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

theorem IsSubmonoid.preimage {M : Type u_1} [] {N : Type u_3} [] {f : MN} (hf : ) {s : Set N} (hs : ) :

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

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

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 '' sProp) :
∀ (x : b f '' s), (∀ (y : M) (hy : y s f y = b), motive )motive x
Equations
• =
Instances For
theorem IsSubmonoid.image {M : Type u_1} [] {γ : Type u_3} [] {f : Mγ} (hf : ) {s : Set M} (hs : ) :

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

theorem Range.isAddSubmonoid {M : Type u_1} [] {γ : Type u_3} [] {f : Mγ} (hf : ) :

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

theorem Range.isSubmonoid {M : Type u_1} [] {γ : Type u_3} [] {f : Mγ} (hf : ) :

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

abbrev IsAddSubmonoid.nsmul_mem.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(∀ (n : ), motive n.succ)motive x
Equations
• =
Instances For
theorem IsAddSubmonoid.nsmul_mem {M : Type u_1} [] {s : Set M} {a : M} (hs : ) (h : a s) {n : } :
n a s

An AddSubmonoid is closed under multiplication by naturals.

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

Submonoids are closed under natural powers.

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

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

theorem IsSubmonoid.powers_subset {M : Type u_1} [] {s : Set M} {a : M} (hs : ) (h : a s) :
s

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

@[deprecated IsSubmonoid.powers_subset]
theorem IsSubmonoid.power_subset {M : Type u_1} [] {s : Set M} {a : M} (hs : ) (h : a s) :
s

Alias of IsSubmonoid.powers_subset.

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

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

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

abbrev IsAddSubmonoid.list_sum_mem.match_1 {M : Type u_1} {s : Set M} (motive : (x : List M) → (x_1x, x_1 s)Prop) :
∀ (x : List M) (x_1 : x_1x, x_1 s), (∀ (x : x[], x s), motive [] x)(∀ (a : M) (l : List M) (h : xa :: l, x s), motive (a :: l) h)motive x x_1
Equations
• =
Instances For
theorem IsSubmonoid.list_prod_mem {M : Type u_1} [] {s : Set M} (hs : ) {l : List M} :
(xl, x s)l.prod 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} [] {s : Set M} (hs : ) (m : ) :
(am, a s)m.sum 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} [] {s : Set M} (hs : ) (m : ) :
(am, a s)m.prod 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 : AM) (motive : (x : ) → (bx, f b s)Prop) :
∀ (x : ) (x_1 : bx, f b s), (∀ (m : ) (hm : m.Nodup) (x : b{ val := m, nodup := hm }, f b s), motive { val := m, nodup := hm } x)motive x x_1
Equations
• =
Instances For
theorem IsAddSubmonoid.finset_sum_mem {M : Type u_3} {A : Type u_4} [] {s : Set M} (hs : ) (f : AM) (t : ) :
(bt, f b s)bt, 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} [] {s : Set M} (hs : ) (f : AM) (t : ) :
(bt, f b s)bt, 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} [] (s : Set A) :
AProp

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

Instances For
inductive Monoid.InClosure {M : Type u_1} [] (s : Set M) :
MProp

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

• basic: ∀ {M : Type u_1} [inst : ] {s : Set M} {a : M}, a s
• one: ∀ {M : Type u_1} [inst : ] {s : Set M},
• mul: ∀ {M : Type u_1} [inst : ] {s : Set M} {a b : M}, Monoid.InClosure s (a * b)
Instances For
def AddMonoid.Closure {M : Type u_1} [] (s : Set M) :
Set M

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

Equations
• = {a : M | }
Instances For
def Monoid.Closure {M : Type u_1} [] (s : Set M) :
Set M

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

Equations
• = {a : M | }
Instances For
theorem AddMonoid.closure.isAddSubmonoid {M : Type u_1} [] (s : Set M) :
theorem Monoid.closure.isSubmonoid {M : Type u_1} [] (s : Set M) :
theorem AddMonoid.subset_closure {M : Type u_1} [] {s : Set M} :

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

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

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

theorem AddMonoid.closure_subset {M : Type u_1} [] {s : Set M} {t : Set M} (ht : ) (h : 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} [] {s : Set M} {t : Set M} (ht : ) (h : 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} [] {s : Set M} {t : Set M} (h : s 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} [] {s : Set M} {t : Set M} (h : s 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} [] {x : M} :

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} [] {x : M} :
=

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} [] {A : Type u_3} [] {f : MA} (hf : ) (s : Set M) :

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} [] {A : Type u_3} [] {f : MA} (hf : ) (s : Set M) :

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} [] {s : Set M} {a : M} (h : ) :
∃ (l : List M), (xl, x s) l.sum = 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} [] {s : Set M} {a : M} (h : ) :
∃ (l : List M), (xl, x s) l.prod = 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_1 {M : Type u_1} [] {s : Set M} {t : Set M} (tl : List M) (motive : (y, z, y + z = tl.sum)Prop) :
∀ (x : y, z, y + z = tl.sum), (∀ (y : M) (hy : ) (z : M) (hz : ) (hyzx : y + z = tl.sum), motive )motive x
Equations
• =
Instances For
abbrev AddMonoid.mem_closure_union_iff.match_3 {M : Type u_1} [] {s : Set M} {t : Set M} {x : M} (motive : (y, z, y + z = x)Prop) :
∀ (x_1 : y, z, y + z = x), (∀ (y : M) (hy : ) (z : M) (hz : ) (hyzx : y + z = x), motive )motive x_1
Equations
• =
Instances For
abbrev AddMonoid.mem_closure_union_iff.match_2 {M : Type u_1} [] {s : Set M} {t : Set M} {x : M} (motive : (∃ (l : List M), (xl, x s t) l.sum = x)Prop) :
∀ (x_1 : ∃ (l : List M), (xl, x s t) l.sum = x), (∀ (L : List M) (HL1 : xL, x s t) (HL2 : L.sum = x), motive )motive x_1
Equations
• =
Instances For
theorem AddMonoid.mem_closure_union_iff {M : Type u_3} [] {s : Set M} {t : Set M} {x : M} :
x AddMonoid.Closure (s t) y, z, 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.

theorem Monoid.mem_closure_union_iff {M : Type u_3} [] {s : Set M} {t : Set M} {x : M} :
x Monoid.Closure (s t) y, z, 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} [] {s : Set M} (h : ) :

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

Equations
• = { carrier := s, add_mem' := , zero_mem' := }
Instances For
def Submonoid.of {M : Type u_1} [] {s : Set M} (h : ) :

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

Equations
• = { carrier := s, mul_mem' := , one_mem' := }
Instances For