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
: ifx ∈ S
whereS
is a multiplicative (resp., additive) submonoid andn
is a natural number, thenx^n
(resp.,n • x
) belongs toS
;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 submonoidsS
,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) ofx
, and a similar result holds for the closure of{x, y}
.
Tags #
submonoid, submonoids
Sum of a list of elements in an AddSubmonoid
is in the AddSubmonoid
.
Sum of a multiset of elements in an AddSubmonoid
of an AddCommMonoid
is
in the AddSubmonoid
.
Product of a multiset of elements in a submonoid of a CommMonoid
is in the submonoid.
Sum of elements in an AddSubmonoid
of an AddCommMonoid
indexed by a Finset
is in the AddSubmonoid
.
Product of elements of a submonoid of a CommMonoid
indexed by a Finset
is in the
submonoid.
Sum of a list of elements in an AddSubmonoid
is in the AddSubmonoid
.
Sum of a multiset of elements in an AddSubmonoid
of an AddCommMonoid
is
in the AddSubmonoid
.
Product of a multiset of elements in a submonoid of a CommMonoid
is in the submonoid.
Sum of elements in an AddSubmonoid
of an AddCommMonoid
indexed by a Finset
is in the AddSubmonoid
.
Product of elements of a submonoid of a CommMonoid
indexed by a Finset
is in the
submonoid.
Equations
- (_ : motive x) = (_ : motive x)
Instances For
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
.
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
.
A dependent version of AddSubmonoid.iSup_induction
.
A dependent version of Submonoid.iSup_induction
.
The submonoid generated by an element of a monoid equals the set of natural number powers of the element.
The submonoid generated by an element.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The submonoid generated by an element is a group if that element has finite order.
Equations
- Submonoid.groupPowers hpos hx = Group.mk (_ : ∀ (y : { x_1 // x_1 ∈ Submonoid.powers x }), y⁻¹ * y = 1)
Instances For
Exponentiation map from natural numbers to powers.
Equations
- Submonoid.pow n m = ↑(MonoidHom.mrangeRestrict (↑(powersHom M) n)) (↑Multiplicative.ofAdd m)
Instances For
Logarithms from powers to natural numbers.
Equations
- Submonoid.log p = Nat.find (_ : ∃ n_1, n ^ n_1 = ↑p)
Instances For
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
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)
Instances For
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)
Instances For
The AddSubmonoid
generated by an element of an AddMonoid
equals the set of
natural number multiples of the element.
The additive submonoid generated by an element.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- (_ : motive x hx) = (_ : motive x hx)
Instances For
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_1 // x_1 ∈ AddSubmonoid.multiples x }), -y + y = 0)
Instances For
Lemmas about additive closures of Subsemigroup
.
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
.
The product of two elements of the additive closure of a submonoid M
is an element of the
additive closure of M
.
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
.
An element is in the closure of a two-element set if it is a linear combination of those two elements.
An element is in the closure of a two-element set if it is a linear combination of those two elements.