Submonoids #
This file provides some results on multiplicative and additive submonoids in the finite context.
theorem
Submonoid.pi_mem_of_mulSingle_mem_aux
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → MulOneClass (f i)]
{S : Type u_3}
[SetLike S ((i : η) → f i)]
[SubmonoidClass S ((i : η) → f i)]
[DecidableEq η]
(I : Finset η)
{H : S}
(x : (i : η) → f i)
(h1 : ∀ i ∉ I, x i = 1)
(h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H)
:
theorem
AddSubmonoid.pi_mem_of_single_mem_aux
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → AddZeroClass (f i)]
{S : Type u_3}
[SetLike S ((i : η) → f i)]
[AddSubmonoidClass S ((i : η) → f i)]
[DecidableEq η]
(I : Finset η)
{H : S}
(x : (i : η) → f i)
(h1 : ∀ i ∉ I, x i = 0)
(h2 : ∀ i ∈ I, Pi.single i (x i) ∈ H)
:
theorem
Submonoid.pi_mem_of_mulSingle_mem
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → MulOneClass (f i)]
{S : Type u_3}
[SetLike S ((i : η) → f i)]
[SubmonoidClass S ((i : η) → f i)]
[Finite η]
[DecidableEq η]
{H : S}
(x : (i : η) → f i)
(h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H)
:
theorem
AddSubmonoid.pi_mem_of_single_mem
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → AddZeroClass (f i)]
{S : Type u_3}
[SetLike S ((i : η) → f i)]
[AddSubmonoidClass S ((i : η) → f i)]
[Finite η]
[DecidableEq η]
{H : S}
(x : (i : η) → f i)
(h : ∀ (i : η), Pi.single i (x i) ∈ H)
:
theorem
Submonoid.pi_le_iff
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → MulOneClass (f i)]
[Finite η]
[DecidableEq η]
{H : (i : η) → Submonoid (f i)}
{J : Submonoid ((i : η) → f i)}
:
For finite index types, the Submonoid.pi
is generated by the embeddings of the monoids.
theorem
AddSubmonoid.pi_le_iff
{η : Type u_1}
{f : η → Type u_2}
[(i : η) → AddZeroClass (f i)]
[Finite η]
[DecidableEq η]
{H : (i : η) → AddSubmonoid (f i)}
{J : AddSubmonoid ((i : η) → f i)}
:
For finite index types, the Submonoid.pi
is generated by the embeddings of the
additive monoids.