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
The proposition that s contains 0.
zero_mem : 0 ∈ sThe proposition that s is closed under addition.
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.
Instances For
The proposition that s contains 1.
one_mem : 1 ∈ sThe proposition that s is closed under multiplication.
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.
Instances For
The intersection of two AddSubmonoid
s of an AddMonoid
M
is an AddSubmonoid
of M.
The intersection of two submonoids of a monoid M
is a submonoid of M
.
The intersection of an indexed set of AddSubmonoid
s of an AddMonoid
M
is
an AddSubmonoid
of M
.
The intersection of an indexed set of submonoids of a monoid M
is a submonoid of M
.
Equations
- isAddSubmonoid_unionᵢ_of_directed.match_3 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
Equations
- isAddSubmonoid_unionᵢ_of_directed.match_2 i j motive x h_1 = Exists.casesOn x fun w h => h_1 w h
The union of an indexed, directed, nonempty set of AddSubmonoid
s of an AddMonoid
M
is an AddSubmonoid
of M
.
Equations
- isAddSubmonoid_unionᵢ_of_directed.match_1 motive hι h_1 = Nonempty.casesOn hι fun val => h_1 val
The union of an indexed, directed, nonempty set of submonoids of a monoid M
is a submonoid
of M
.
Equations
- multiples.add_mem.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
The set of natural number multiples of an element of an AddMonoid
M
is
an AddSubmonoid
of M
.
The set of natural number powers of an element of a monoid M
is a submonoid of M
.
An AddMonoid
is an AddSubmonoid
of itself.
A monoid is a submonoid of itself.
The preimage of an AddSubmonoid
under an AddMonoid
hom is
an AddSubmonoid
of the domain.
The preimage of a submonoid under a monoid hom is a submonoid of the domain.
The image of an AddSubmonoid
under an AddMonoid
hom is an AddSubmonoid
of the
codomain.
Equations
- IsAddSubmonoid.image.match_1 b motive x h_1 = Exists.casesOn x fun w h => h_1 w h
The image of a submonoid under a monoid hom is a submonoid of the codomain.
The image of an AddMonoid
hom is an AddSubmonoid
of the codomain.
The image of a monoid hom is a submonoid of the codomain.
Equations
- IsAddSubmonoid.nsmul_mem.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
An AddSubmonoid
is closed under multiplication by naturals.
The set of natural number multiples of an element of an AddSubmonoid
is a subset of
the AddSubmonoid
.
The set of natural number powers of an element of a submonoid is a subset of the submonoid.
The sum of a list of elements of an AddSubmonoid
is an element of the AddSubmonoid
.
The sum of a multiset of elements of an AddSubmonoid
of an AddCommMonoid
is an element of the AddSubmonoid
.
The product of a multiset of elements of a submonoid of a CommMonoid
is an element of
the submonoid.
The sum of elements of an AddSubmonoid
of an AddCommMonoid
indexed by
a Finset
is an element of the AddSubmonoid
.
Equations
- IsAddSubmonoid.finset_sum_mem.match_1 f motive x x h_1 = Finset.casesOn A (fun x => (x_1 : ∀ (b : A), b ∈ x → f b ∈ s) → motive x x_1) x (fun val nodup x => h_1 val nodup x) x
The product of elements of a submonoid of a CommMonoid
indexed by a Finset
is an element
of the submonoid.
- basic: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A} {a : A}, a ∈ s → AddMonoid.InClosure s a
- zero: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A}, AddMonoid.InClosure s 0
- add: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A} {a b : A}, AddMonoid.InClosure s a → AddMonoid.InClosure s b → AddMonoid.InClosure s (a + b)
The inductively defined membership predicate for the submonoid generated by a subset of a monoid.
Instances For
- 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)
The inductively defined membership predicate for the Submonoid
generated by a subset of an
monoid.
Instances For
The inductively defined AddSubmonoid
genrated by a subset of an AddMonoid
.
Equations
- AddMonoid.Closure s = { a | AddMonoid.InClosure s a }
The inductively defined submonoid generated by a subset of a monoid.
Equations
- Monoid.Closure s = { a | Monoid.InClosure s a }
A subset of an AddMonoid
is contained in the AddSubmonoid
it generates.
A subset of a monoid is contained in the submonoid it generates.
The AddSubmonoid
generated by a set is contained in any AddSubmonoid
that
contains the set.
The submonoid generated by a set is contained in any submonoid that contains the set.
Given subsets t
and s
of an AddMonoid M
, if s ⊆ t⊆ t
, the AddSubmonoid
of M
generated by s
is contained in the AddSubmonoid
generated by t
.
The AddSubmonoid
generated by an element of an AddMonoid
equals the set of
natural number multiples of the element.
The submonoid generated by an element of a monoid equals the set of natural number powers of the element.
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.
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.
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
.
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
.
Equations
- One or more equations did not get rendered due to their size.
Given sets s, t
of a commutative AddMonoid M
, x ∈ M∈ M
is in the AddSubmonoid
of M
generated by s ∪ t∪ 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
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddMonoid.mem_closure_union_iff.match_2 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Given sets s, t
of a commutative monoid M
, x ∈ M∈ M
is in the submonoid of M
generated by
s ∪ t∪ 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
.
Create a bundled additive submonoid from a set s
and [IsAddSubmonoid s]
.
Create a bundled submonoid from a set s
and [IsSubmonoid s]
.