Subgroup.card_bot
theorem Subgroup.card_bot : ∀ {G : Type u_1} [inst : Group G] {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1
This theorem, `Subgroup.card_bot`, states that for any type `G` which is a group, the number of elements in the bottom subgroup (denoted by `⊥`) is always equal to 1. Here, `⊥` represents the trivial subgroup which contains only the group's identity element. Thus, regardless of the specific group `G` we are dealing with, the cardinality of this trivial subgroup is always 1.
More concisely: The cardinality of the trivial subgroup of any group is 1.
|
AddSubgroup.list_sum_mem
theorem AddSubgroup.list_sum_mem :
∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {l : List G}, (∀ x ∈ l, x ∈ K) → l.sum ∈ K
This theorem states that for any additive group G and its additive subgroup K, the sum of a list of elements that are all in K is also in K. In other words, if we take a list of elements from the subgroup, and add them all together, the result is still in the subgroup. This is a theorem about the closure property of subgroups in the context of additive groups.
More concisely: If G is an additive group and K is a subgroup of G, then the sum of any list of elements from K is also an element of K.
|
Subgroup.eq_top_of_card_eq
theorem Subgroup.eq_top_of_card_eq :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : Fintype ↥H] [inst_2 : Fintype G],
Fintype.card ↥H = Fintype.card G → H = ⊤
This theorem states that for any group `G` and any subgroup `H` of `G`, if the number of elements in `H` (denoted as `Fintype.card ↥H`) is equal to the number of elements in `G` (denoted as `Fintype.card G`), then the subgroup `H` must be equal to the entire group `G`. In other words, if a subgroup and the group have the same cardinality, the subgroup is the whole group.
More concisely: If a subgroup of a group has the same number of elements as the group, then the subgroup is equal to the group.
|
Subgroup.multiset_prod_mem
theorem Subgroup.multiset_prod_mem :
∀ {G : Type u_3} [inst : CommGroup G] (K : Subgroup G) (g : Multiset G), (∀ a ∈ g, a ∈ K) → g.prod ∈ K
The `Subgroup.multiset_prod_mem` theorem states that for any type `G` that forms a commutative group, given a subgroup `K` of the group and a multiset `g` of elements from the group, if every element of the multiset is in the subgroup `K`, then the product of the elements in the multiset is also an element of the subgroup `K`. This theorem reflects the closure property of a subgroup in the context of multisets.
More concisely: If `G` is a commutative group, `K` is a subgroup of `G`, and every element in the multiset `g` of `G` belongs to `K`, then the product of the elements in `g` belongs to `K`.
|
Subgroup.list_prod_mem
theorem Subgroup.list_prod_mem :
∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {l : List G}, (∀ x ∈ l, x ∈ K) → l.prod ∈ K
This theorem states that, for any type `G` that forms a group, and any subgroup `K` of that group, the product of a list of elements from `G` is included in `K`, provided that each element in the list is also in `K`. In other words, if all elements of the list belong to the subgroup, then their product also belongs to the same subgroup.
More concisely: If `G` is a group and `K` is a subgroup of `G`, then the product of any list of elements from `G` that belong to `K` also belongs to `K`.
|
Subgroup.pi_le_iff
theorem Subgroup.pi_le_iff :
∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [inst_1 : DecidableEq η] [inst_2 : Finite η]
{H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)},
Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J
This theorem states that for any finite index type `η`, given any family of subgroups indexed by `η` (`H : (i : η) → Subgroup (f i)`), and any subgroup `J` of the dependent function type `(i : η) → f i`, the subgroup of dependent functions whose components all belong to the respective subgroups (`Subgroup.pi Set.univ H`) is a subgroup of `J` if and only if for every index `i` in `η`, the image of the `i`th subgroup `H i` under the monoid homomorphism embedding it into the dependent function type at the `i`th component (`MonoidHom.mulSingle f i`) is a subgroup of `J`.
In simpler language, it says that a set of functions from an index set to different groups is a subgroup of another if and only if each of the individual group components, when considered as a function constant everywhere except at one point, is a subgroup of the latter.
More concisely: A family of subgroups indexed by a finite type is a subgroup of a dependent function type if and only if the image of each index's subgroup under the monoid homomorphism embedding it into the dependent function type is a subgroup.
|
AddSubgroup.pi_le_iff
theorem AddSubgroup.pi_le_iff :
∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → AddGroup (f i)] [inst_1 : DecidableEq η] [inst_2 : Finite η]
{H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)},
AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (H i) ≤ J
The theorem `AddSubgroup.pi_le_iff` states that for finite index types, the additive subgroup of dependent functions, denoted as `AddSubgroup.pi Set.univ H`, is subordinate to another additive subgroup `J`, if and only if, for every index `i`, the image of the additive subgroup `H i` under the embedding of the additive group `AddMonoidHom.single f i` is also subordinate to `J`. Here, 'subordinate to' means 'is a subset of' in terms of set theory.
In more formal terms, if η is a finite index type and `f` is a family of additive groups indexed by η, and `H` is a family of subgroups of these additive groups, then `AddSubgroup.pi Set.univ H` (the dependent product of these subgroups) is contained in another additive subgroup `J` if and only if for each index `i` in η, the image of `H i` under the additive monoid homomorphism `AddMonoidHom.single f i` (which embeds `H i` into the dependent product) is also contained in `J`.
More concisely: A family of subgroups `H` of an indexed family of additive groups `(AddMonoid H i : i ∈ η)` forms a subgroup of another additive subgroup `J`, if and only if, for every index `i`, the image of `H i` under the embedding of `H i` into the dependent product `AddSubgroup.pi Set.univ H` is also a subset of `J`.
|
AddSubgroup.multiset_sum_mem
theorem AddSubgroup.multiset_sum_mem :
∀ {G : Type u_3} [inst : AddCommGroup G] (K : AddSubgroup G) (g : Multiset G), (∀ a ∈ g, a ∈ K) → g.sum ∈ K := by
sorry
This theorem states that for any given type `G` that is an instance of an additive commutative group, and for any additive subgroup `K` of `G`, if all elements of a multiset `g` are in `K`, then the sum of all elements in the multiset `g` is also in `K`. In other words, the sum of a multiset of elements in an additive subgroup of an additive commutative group is still in the same additive subgroup.
More concisely: For any additive commutative group `G` and its additive subgroup `K`, if all elements in a multiset `g` belong to `K`, then the sum of `g` belongs to `K` as well.
|
AddSubgroup.eq_top_of_card_eq
theorem AddSubgroup.eq_top_of_card_eq :
∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : Fintype ↥H] [inst_2 : Fintype G],
Fintype.card ↥H = Fintype.card G → H = ⊤
The theorem `AddSubgroup.eq_top_of_card_eq` states that for any additive group `G` and any of its additive subgroups `H`, given that both `G` and `H` are finite (`Fintype G` and `Fintype ↥H`, where `↥H` represents the set of elements in `H`), if the number of elements in the subgroup `H` (`Fintype.card ↥H`) is equal to the number of elements in the group `G` (`Fintype.card G`), then the subgroup `H` must be equal to the entire group `G` (denoted `⊤`). In other words, if a finite group and one of its subgroups have the same cardinality, then the subgroup must in fact be the whole group.
More concisely: If two finite additive groups have equal cardinalities, then the smaller subgroup is equal to the larger group.
|
Subgroup.prod_mem
theorem Subgroup.prod_mem :
∀ {G : Type u_3} [inst : CommGroup G] (K : Subgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G},
(∀ c ∈ t, f c ∈ K) → (t.prod fun c => f c) ∈ K
This theorem states that for any commutative group `G`, and any subgroup `K` within `G`, if we have a finite set `t` indexed by an arbitrary type `ι` and a function `f` mapping each element of `t` to a group element, then the product of all the group elements corresponding to each element of `t` is still in the subgroup `K`. This holds true provided that each group element `f c` generated by applying the function `f` to an element `c` in the set `t` is in the subgroup `K`.
More concisely: If `G` is a commutative group, `K` is a subgroup of `G`, and for all `c` in a set `t` indexed by an arbitrary type `ι`, `f c` is in `K` implies the product of `f c` for all `c` in `t` is in `K`.
|
AddSubgroup.sum_mem
theorem AddSubgroup.sum_mem :
∀ {G : Type u_3} [inst : AddCommGroup G] (K : AddSubgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G},
(∀ c ∈ t, f c ∈ K) → (t.sum fun c => f c) ∈ K
This theorem states that for any commutative additive group `G` and any subgroup `K` of `G`, the sum of any finite set of elements from this subgroup (which can be mapped through a function `f` from a finite set `t` indexed by `ι`) remains in the subgroup `K`. In other words, the sum of elements from an additive subgroup of a commutative additive group, indexed by a finite set, is still an element of the subgroup.
More concisely: For any commutative additive group `G` and subgroup `K`, the sum of elements from `K` indexed by a finite set remains in `K`.
|