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_supᵢ_of_directed
,coe_supᵢ_of_directed
,mem_supₛ_of_directedOn
,coe_supₛ_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.
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
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
- AddSubmonoid.mem_supᵢ_of_directed.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
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.supᵢ_induction
.
A dependent version of Submonoid.supᵢ_induction
.
The submonoid generated by an element of a monoid equals the set of natural number powers of the element.
Exponentiation map from natural numbers to powers.
Equations
- Submonoid.pow n m = ↑(MonoidHom.mrangeRestrict (↑(powersHom M) n)) (↑Multiplicative.ofAdd m)
Logarithms from powers to natural numbers.
Equations
- Submonoid.log p = Nat.find (_ : ∃ n, n ^ n = ↑p)
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.
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)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a : { x // x ∈ AddSubmonoid.closure s }), 0 + a = a) = (_ : ∀ (a : { x // x ∈ AddSubmonoid.closure s }), 0 + a = a)
Equations
- (_ : ∀ (x : { x // x ∈ AddSubmonoid.closure s }), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : { x // x ∈ AddSubmonoid.closure s }), AddMonoid.nsmul 0 x = 0)
Equations
- (_ : ∀ (a : { x // x ∈ AddSubmonoid.closure s }), a + 0 = a) = (_ : ∀ (a : { x // x ∈ AddSubmonoid.closure s }), a + 0 = a)
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)
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.
Equations
- One or more equations did not get rendered due to their size.
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.