AddSubgroup.relindex_bot_left
theorem AddSubgroup.relindex_bot_left :
∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⊥.relindex H = Nat.card ↥H
This theorem states that for any given additive group `G` and any subgroup `H` of `G`, the relative index of the trivial subgroup (denoted as `⊥`) with respect to `H` is equal to the cardinality (or the number of elements) of `H`. In other words, the number of distinct cosets formed by partitioning `H` with the trivial subgroup is the same as the number of elements in `H`, when we consider the cardinality of an infinite set as zero.
More concisely: The relative index of the trivial subgroup in an additive group `G` with respect to a subgroup `H` equals the cardinality of `H`.
|
AddSubgroup.relindex_eq_zero_of_le_right
theorem AddSubgroup.relindex_eq_zero_of_le_right :
∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, K ≤ L → H.relindex K = 0 → H.relindex L = 0 := by
sorry
This theorem states that, for any group `G` with an associated addition operation, and given three subgroups `H`, `K`, and `L` of `G`, if `K` is a subset of `L` and the relative index of `H` and `K` is zero, then the relative index of `H` and `L` will also be zero. The relative index of two subgroups here is defined as the index of the intersection subgroup of `H` and `K` in `K`, or it is zero if the relative index is infinite.
More concisely: If subgroup `H` of group `G` has zero relative index with respect to a larger subgroup `K`, and `K` is contained in another subgroup `L` of `G`, then `H` has zero relative index with respect to `L`.
|
Subgroup.index_dvd_of_le
theorem Subgroup.index_dvd_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → K.index ∣ H.index := by
sorry
This theorem states that for any given group `G`, if `H` and `K` are subgroups of `G` and `H` is a subgroup of `K`, then the index of `K` in `G` divides the index of `H` in `G`. Here, the index of a subgroup is defined as the cardinality of the set of all left cosets of the subgroup in the group, or it is zero if this set is infinite. The theorem is about an important property of the index function in group theory.
More concisely: If `H` is a subgroup of `K` and `K` is a subgroup of group `G`, then the index of `H` in `G` is a multiple of the index of `K` in `G`.
|
Subgroup.index_bot
theorem Subgroup.index_bot : ∀ {G : Type u_1} [inst : Group G], ⊥.index = Nat.card G
This theorem states that for any given group `G`, the index of the trivial subgroup (denoted as `⊥`) is equal to the cardinality of the group `G`. In mathematical terms, for a group `G`, the number of left cosets of the trivial subgroup in `G` (which is the index of this subgroup), is equal to the number of elements in `G`. Note that the cardinality of a group is the number of elements in the group and here it's represented as a natural number using `Nat.card`. If the group `G` is infinite, both the index of the trivial subgroup and the cardinality of the group `G` would be zero, as per the definitions.
More concisely: The index of the trivial subgroup in a group equals its cardinality. (If the group is infinite, both are zero.)
|
Subgroup.relindex_mul_index
theorem Subgroup.relindex_mul_index :
∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → H.relindex K * K.index = H.index
This theorem states that for any given group `G` and two subgroups `H` and `K` of `G`, if `H` is a subgroup of `K`, then the product of the relative index of `H` in `K` and the index of `K` in `G` is equal to the index of `H` in `G`. The relative index of a subgroup is the natural number that represents the index of the subgroup in the larger group, and it returns 0 if the relative index is infinite. Similarly, the index of a subgroup is the size of the set of cosets of the subgroup in the group, represented as a natural number, and returns 0 if the index is infinite.
More concisely: For any groups G, H, and K with H a subgroup of K, the product of the relative index of H in K and the index of K in G equals the index of H in G.
|
Mathlib.GroupTheory.Index._auxLemma.12
theorem Mathlib.GroupTheory.Index._auxLemma.12 :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.index = H.relindex ⊤
The theorem `Mathlib.GroupTheory.Index._auxLemma.12` states that for any given group `G` and any subgroup `H` of `G`, the index of `H` is equal to the relative index of `H` with respect to the total group `G`. Here, the index of a subgroup is defined as the number of its cosets, and returns 0 if the index is infinite. The relative index of a subgroup is similar but is measured with respect to another subgroup, in this case, the total group `G`.
More concisely: The theorem `Mathlib.GroupTheory.Index._auxLemma.12` asserts that the index of a subgroup in a group equals its relative index with respect to the total group.
|
AddSubgroup.inf_relindex_right
theorem AddSubgroup.inf_relindex_right :
∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), (H ⊓ K).relindex K = H.relindex K
The theorem `AddSubgroup.inf_relindex_right` states that for any given additive group `G` and any two subgroups `H` and `K` of `G`, the relative index of the intersection of `H` and `K` with respect to `K` is the same as the relative index of `H` with respect to `K`. Here, the relative index of a subgroup is a natural number that measures the "size" of the subgroup compared to another subgroup, and it returns 0 if the relative index is infinite.
More concisely: The relative index of a subgroup `H` with respect to `K` in an additive group `G` equals the relative index of `H` intersected with `K` with respect to `K`.
|
AddSubgroup.FiniteIndex.finiteIndex
theorem AddSubgroup.FiniteIndex.finiteIndex :
∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G} [self : H.FiniteIndex], H.index ≠ 0
This theorem states that for any given additive subgroup (`H`) of an additive group (`G`), if this subgroup has a finite index (denoted by `H.FiniteIndex`), then the index of the subgroup `H` is not equal to zero. Here, the index refers to the number of distinct cosets of the subgroup in the group.
More concisely: If `H` is an additive subgroup of an additive group `G` with finite index, then the index of `H` in `G` is non-zero.
|
Subgroup.index_eq_card
theorem Subgroup.index_eq_card :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : Fintype (G ⧸ H)], H.index = Fintype.card (G ⧸ H) := by
sorry
The theorem `Subgroup.index_eq_card` states that for any group `G` and any subgroup `H` of `G` such that the quotient group `G ⧸ H` is finite, the index of the subgroup `H` in `G` (which is represented as a natural number or zero if the index is infinite) equals the number of elements in the quotient group `G ⧸ H`.
More concisely: For any finite quotient group G/H of a group G, the index of subgroup H in G equals the number of elements in G/H.
|
Subgroup.index_comap
theorem Subgroup.index_comap :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {G' : Type u_2} [inst_1 : Group G'] (f : G' →* G),
(Subgroup.comap f H).index = H.relindex f.range
The theorem `Subgroup.index_comap` states that for any Group `G`, `G'` and a subgroup `H` of `G`, as well as a monoid homomorphism `f` from `G'` to `G`, the index (as a natural number) of the preimage of `H` along `f` (found using `Subgroup.comap`) is equal to the relative index of `H` with respect to the range of `f` (found using `Subgroup.relindex` and `MonoidHom.range`). In other words, it provides a relationship between the index of the preimage of a subgroup under a monoid homomorphism and the relative index of the subgroup and the range of the homomorphism.
More concisely: The index of the preimage of a subgroup under a monoid homomorphism is equal to the relative index of the subgroup with respect to the range of the homomorphism.
|
AddSubgroup.index_eq_one
theorem AddSubgroup.index_eq_one : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 1 ↔ H = ⊤ := by
sorry
This theorem states that for any given type `G` that forms an additive group, and for any subgroup `H` of this group, the index of `H` is equal to one if and only if `H` is a top element. In mathematical terms, it means that if the quotient space formed by the group `G` and its subgroup `H` has just one element (i.e., the index of `H` in `G` is one), then `H` must be the whole group `G` itself. Conversely, if `H` is the whole group `G`, then the index of `H` in `G` is one.
More concisely: For an additive group `G` and its subgroup `H`, the index of `H` in `G` equals 1 if and only if `H` is the whole group `G`.
|
AddSubgroup.index_eq_two_iff
theorem AddSubgroup.index_eq_two_iff :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b + a ∈ H) (b ∈ H)
This theorem states that for any additive group `G` and an additive subgroup `H` of `G`, `H` has an index of two if and only if there exists an element `a` in `G` such that for every element `b` in `G`, exactly one of `b + a` and `b` belongs to `H`. Here existence of exactly one of `b + a` and `b` in `H` means that either `b + a` is in `H` and `b` is not, or `b` is in `H` and `b + a` is not.
More concisely: A subgroup H of an additive group G has index 2 if and only if there exists an element a in G such that for all b in G, exactly one of b and b + a belongs to H.
|
Subgroup.index_top
theorem Subgroup.index_top : ∀ {G : Type u_1} [inst : Group G], ⊤.index = 1
This theorem states that for any given Type `G` that forms a Group, the index of the top (or universal) subgroup is always equal to 1. In mathematical terms, if `G` is a group, then the index of the top subgroup (which contains all elements of the group) is 1. This is because the top subgroup is essentially the whole group itself, and the index of a group to itself is defined as 1.
More concisely: The index of a group to itself is equal to 1. (For any group G, |G| := |{x : G | x = 0}| = 1)
|
Subgroup.index_eq_two_iff
theorem Subgroup.index_eq_two_iff :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H) := by
sorry
The theorem `Subgroup.index_eq_two_iff` states that, for any given group `G` and subgroup `H` of `G`, `H` has an index of two if and only if there exists an element `a` from the group such that for all elements `b` from `G`, exactly one of `b * a` and `b` belongs to `H`. Here, the belonging to `H` is exclusive in the sense that if `b * a` belongs to `H`, then `b` does not belong to `H` and vice versa. This exclusivity is defined by the `Xor'` function which captures the logical XOR (exclusive or) operation.
More concisely: A subgroup of a group has index 2 if and only if there exists an element such that the subgroup contains exactly one of each pair of elements and their product.
|
AddSubgroup.index_top
theorem AddSubgroup.index_top : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.index = 1
The theorem `AddSubgroup.index_top` states that for any type `G` that has an additive group structure, the index of the entire set (denoted by `⊤`) as a subgroup of itself is 1. In mathematical terms, if `G` is an additive group, then the index (or the number of distinct cosets) of `G` as a subgroup of `G` is one.
More concisely: For any additive group G, the index of G as a subgroup of itself is equal to 1.
|
Subgroup.FiniteIndex.finiteIndex
theorem Subgroup.FiniteIndex.finiteIndex :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [self : H.FiniteIndex], H.index ≠ 0
This theorem states that for any group `G` and any subgroup `H` of `G`, if `H` has a finite index in `G`, then the index of `H` in `G` is not zero. In terms of group theory, the index of a subgroup in a group is the number of its left cosets in the group. So this theorem ensures that if the number of left cosets of subgroup `H` in group `G` is finite, it cannot be zero.
More concisely: If `H` is a subgroup of a group `G` with finite index, then the index of `H` in `G` is non-zero.
|
Subgroup.index_eq_one
theorem Subgroup.index_eq_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 1 ↔ H = ⊤
This theorem states that for any group `G` and subgroup `H` of `G`, the index of `H` in `G` is equal to one if and only if `H` is the entire group `G`. Here, the index of a subgroup is defined as the number of distinct cosets of the subgroup in the group, and the symbol `⊤` represents the whole group. If the index is infinite, the index function returns 0.
More concisely: A subgroup of a group is the entire group if and only if its index is equal to 1. (In other words, a subgroup is the identity subgroup if and only if every coset is identical to the group itself.)
|
AddSubgroup.index_comap
theorem AddSubgroup.index_comap :
∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [inst_1 : AddGroup G'] (f : G' →+ G),
(AddSubgroup.comap f H).index = H.relindex f.range
The theorem `AddSubgroup.index_comap` states that for any additive group `G`, any subgroup `H` of `G`, any other additive group `G'`, and any additive monoid homomorphism `f` from `G'` to `G`, the index of the preimage of `H` under `f` is equal to the relative index of `H` in the range of `f`. In other words, the size of the group obtained by applying `f` to `G'` and taking the set of elements that land in `H`, viewed as a multiple of the size of `H`, is the same as the size of the group obtained by considering all possible destinations of `f` inside `G`, viewed as a multiple of the size of `H` inside the group of such destinations.
More concisely: The index of the preimage of a subgroup under an additive monoid homomorphism is equal to the relative index of the subgroup in the range of the homomorphism.
|
Subgroup.inf_relindex_right
theorem Subgroup.inf_relindex_right :
∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), (H ⊓ K).relindex K = H.relindex K
This theorem states that for any type `G` with a group structure and for any two subgroups `H` and `K` of `G`, the relative index of the intersection of `H` and `K` with `K` is equal to the relative index of `H` with `K`. In mathematical terms, it asserts that if `H` and `K` are subgroups of a group `G`, then the relative index of `H ∩ K` in `K` (`[K : H ∩ K]`) is equal to the relative index of `H` in `K` (`[K : H]`). This relative index is defined as the index of the subgroup formed by the subset of `H` within `K` (or equivalently, the quotient of the order of `K` by the order of `H`), giving the number of left cosets of `H` in `K`, or returning zero if this number is infinite.
More concisely: For any groups G, H, and K with H, K subgroups of G, the index of H in K equals the index of H ∩ K in K.
|
Subgroup.index_ne_zero_of_finite
theorem Subgroup.index_ne_zero_of_finite :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : Finite (G ⧸ H)], H.index ≠ 0
This theorem asserts that for any group `G` and its subgroup `H`, if the quotient group `G/H` (the set of all left cosets of `H` in `G`) is finite, then the index of `H` in `G` (the number of distinct left cosets of `H` in `G`) is not equal to zero. This simply means when the quotient group is finite, there is at least one distinct left coset of `H` in `G`.
More concisely: If `G` is a group and `H` is a subgroup of `G` such that the quotient group `G/H` is finite, then the index of `H` in `G` is nonzero.
|
AddSubgroup.relindex_mul_index
theorem AddSubgroup.relindex_mul_index :
∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → H.relindex K * K.index = H.index
This theorem states that for any additive group `G` and any two of its subgroups `H` and `K` such that `H` is a subgroup of `K`, the product of the relative index of `H` in `K` and the index of `K` equals the index of `H`. Here, the relative index of a subgroup is defined as the index of the subgroup formed from the original subgroup and another subgroup, and the index of a subgroup is defined as the cardinality of the quotient group formed by the group and the subgroup. Note that indices are given as natural numbers and are zero in case of infinite indices.
More concisely: For any additive group `G` and subgroups `H` and `K` with `H` a subgroup of `K`, the product of the index of `H` in `K` and the index of `K` in `G` equals the index of `H` in `G`.
|
Subgroup.card_mul_index
theorem Subgroup.card_mul_index :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nat.card ↥H * H.index = Nat.card G
This theorem states that for any group `G` and any subgroup `H` of `G`, the product of the cardinality of `H` (represented as a natural number) and the index of `H` in `G` (also represented as a natural number) equals the cardinality of `G`. In other words, if we denote the cardinality of a set `X` as `|X|`, the theorem asserts that `|H| * [G : H] = |G|`, where `[G : H]` denotes the index of the subgroup `H` in `G`. This is a generalization of Lagrange's Theorem for finite groups to possibly infinite groups, with the understanding that the cardinality and index are interpreted as natural numbers, and an "infinite" cardinality is represented by the natural number 0.
More concisely: For any group `G` and subgroup `H`, the product of the cardinalities of `H` and its index in `G` equals the cardinality of `G`.
|
AddSubgroup.index_bot
theorem AddSubgroup.index_bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.index = Nat.card G
This theorem states that for every type `G` that has an additive group structure, the index of the trivial subgroup (denoted by `⊥`) in `G` is equal to the cardinality of `G` as a natural number. The index of a subgroup is defined as the number of its left or right cosets, and in this case, we are considering the unique subgroup that contains only the additive identity element. The cardinality of `G` is the number of distinct elements in `G`. If `G` is infinite, both the index and cardinality are defined as 0.
More concisely: For every additive group `G`, the number of cosets of the trivial subgroup equals the cardinality of `G`.
|
Mathlib.GroupTheory.Index._auxAddLemma.12
theorem Mathlib.GroupTheory.Index._auxAddLemma.12 :
∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.index = H.relindex ⊤
This theorem states that for any additive group `G` and its subgroup `H`, the index of `H` is equal to the relative index of `H` with respect to the entire group `G` (denoted by `⊤`). In other words, the number of distinct cosets of `H` in `G` is the same as the count of distinct cosets when considering `G` itself as the larger subgroup. The index returns 0 in the case of infinite number of cosets.
More concisely: For any additive group `G` and its subgroup `H`, the number of cosets of `H` in `G` equals the order of `G/H`.
|
Subgroup.relindex_bot_left
theorem Subgroup.relindex_bot_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⊥.relindex H = Nat.card ↥H
This theorem states that for any given group `G` and a subgroup `H` of `G`, the relative index of the trivial subgroup (denoted by `⊥`) and `H` is equal to the cardinality of `H` expressed as a natural number. In other words, this is saying that the number of cosets of `H` in the trivial subgroup is equal to the number of elements in `H`. This makes sense since the trivial subgroup contains only the identity element of the group, so each element of `H` forms its own coset.
More concisely: The relative index of the trivial subgroup and a subgroup `H` of a group `G` is equal to the cardinality of `H`.
|
Subgroup.relindex_eq_zero_of_le_right
theorem Subgroup.relindex_eq_zero_of_le_right :
∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, K ≤ L → H.relindex K = 0 → H.relindex L = 0
This theorem states that for any type `G` that forms a group, and for any three subgroups `H`, `K`, and `L` of `G`, if `K` is a subset of `L` and the relative index of `H` and `K` is zero, then the relative index of `H` and `L` is also zero. The relative index of two subgroups `H` and `K` is defined as the index of the subgroup formed by `H` and `K`, and is zero if this index is infinite.
More concisely: For any groups `G`, `H`, `K`, and `L` where `K` is a subset of `L` and the index of `H` in `K` is finite and equal to 1, the index of `H` in `L` is also equal to 1. (Or, if the index is infinite, then it is zero.)
|
AddSubgroup.relindex_eq_zero_of_le_left
theorem AddSubgroup.relindex_eq_zero_of_le_left :
∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, H ≤ K → K.relindex L = 0 → H.relindex L = 0 := by
sorry
This theorem states that for any additive group `G` and any three of its subgroups `H`, `K`, and `L`, if `H` is a subgroup of (or equal to) `K` and the relative index (as a natural number) of `K` and `L` is zero, then the relative index of `H` and `L` is also zero. The relative index of two subgroups here is defined as the index of the subgroup formed by their intersection, and it returns 0 if this relative index is infinite.
More concisely: If subgroups H, K, and L of an additive group G have H a subgroup of (or equal to) K and the index of K in L is finite and equal to one, then the index of H in L is also finite and equal to one.
|
Subgroup.relindex_eq_zero_of_le_left
theorem Subgroup.relindex_eq_zero_of_le_left :
∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H ≤ K → K.relindex L = 0 → H.relindex L = 0
This theorem states that for any group G and any three of its subgroups H, K, and L, if H is a subgroup of K and the relative index of K and L is zero (which means either K is not a subgroup of L or K and L have infinite index), then the relative index of H and L is also zero. This theorem captures a certain transitivity property of the relative index in the context of subgroups of a given group.
More concisely: If H is a subgroup of K and the index of K in L is infinite, then the index of H in L is also infinite. (Or, more precisely, if the index of K in L is 0, then the index of H in L is also 0, under the assumption that H is a subgroup of K.)
|