Subgroup.mem_zpowers_iff
theorem Subgroup.mem_zpowers_iff :
∀ {G : Type u_1} [inst : Group G] {g h : G}, h ∈ Subgroup.zpowers g ↔ ∃ k, g ^ k = h
This theorem is about the membership of an element in the subgroup generated by another element in a group. For any group `G`, and any two elements `g` and `h` of `G`, `h` is in the subgroup generated by `g` if and only if there exists an integer `k` such that `g` raised to the power of `k` equals `h`. In mathematical terms, this is saying that $h \in \langle g \rangle$ if and only if $\exists k \in \mathbb{Z}, g^k = h$. The theorem provides a condition for membership in the cyclic subgroup generated by a given group element.
More concisely: A group element `h` belongs to the subgroup generated by another element `g` if and only if there exists an integer `k` such that `g^k = h`.
|
Subgroup.zpowers_eq_closure
theorem Subgroup.zpowers_eq_closure :
∀ {G : Type u_1} [inst : Group G] (g : G), Subgroup.zpowers g = Subgroup.closure {g}
This theorem states that for any group `G` and any element `g` from `G`, the subgroup generated by the powers of `g` (denoted as `Subgroup.zpowers g`) is the same as the subgroup generated by the singleton set containing `g` (denoted as `Subgroup.closure {g}`). In other words, both methods of generating a subgroup - one by considering all powers of a given element and the other by taking the closure of a set containing just that element - yield the same result.
More concisely: For any group `G` and element `g` from `G`, the subgroup generated by the powers of `g` equals the subgroup generated by `{g}`.
|
AddSubgroup.mem_zmultiples_iff
theorem AddSubgroup.mem_zmultiples_iff :
∀ {G : Type u_1} [inst : AddGroup G] {g h : G}, h ∈ AddSubgroup.zmultiples g ↔ ∃ k, k • g = h
This theorem states that for any additively group-structured type `G` and any two elements `g` and `h` of `G`, `h` is in the subgroup generated by `g` if and only if there exists an integer `k` such that `k` times `g` equals `h`. In other words, an element `h` is in the subgroup produced by repeatedly adding `g` to itself if and only if `h` itself can be expressed as `g` added to itself a certain number of times.
More concisely: An element `h` of an additively group-structured type `G` is in the subgroup generated by an element `g` if and only if there exists an integer `k` such that `h = k * g`.
|
AddSubgroup.mem_zmultiples
theorem AddSubgroup.mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), g ∈ AddSubgroup.zmultiples g := by
sorry
This theorem states that for any given additive group `G` and an element `g` in `G`, `g` is an element of the subgroup generated by `g` itself. In other words, every element in an additive group is in the additive subgroup generated by itself. This is a fundamental property of groups in mathematics: any element of a group forms a cyclic subgroup with itself.
More concisely: Every element in an additive group is in the subgroup generated by that element itself.
|
Subgroup.mem_zpowers
theorem Subgroup.mem_zpowers : ∀ {G : Type u_1} [inst : Group G] (g : G), g ∈ Subgroup.zpowers g
This theorem states that for any group `G` and any element `g` in the group, `g` is a member of the subgroup generated by `g`. Specifically, the `Subgroup.zpowers g` is the subgroup of `G` generated by powers of `g` (i.e., all elements of the form `g^n` for integers `n`). The theorem asserts that `g` itself (which can be considered as `g` to the power of 1) is a member of this subgroup.
More concisely: For any group `G` and any of its element `g`, `g` is an element of the subgroup generated by `g` (i.e., `Subgroup.zpowers g`).
|
Subgroup.zpowers_le_of_mem
theorem Subgroup.zpowers_le_of_mem :
∀ {G : Type u_1} [inst : Group G] {g : G} {H : Subgroup G}, g ∈ H → Subgroup.zpowers g ≤ H
The theorem `Subgroup.zpowers_le_of_mem` is an alias for the reverse direction of `Subgroup.zpowers_le`. It states that for any type `G` that has a group structure, given any element `g` of `G` and a subgroup `H` of `G`, if `g` is an element of `H`, then the subgroup generated by `g` (denoted by `Subgroup.zpowers g`) is a subset of (or equal to) `H`. This essentially means that if a group element is in a subgroup, then the subgroup generated by that element is contained within the original subgroup.
More concisely: If `g` is an element of the subgroup `H` of a group `G`, then the subgroup generated by `g` is contained in `H`.
|
AddSubgroup.zmultiples_eq_bot
theorem AddSubgroup.zmultiples_eq_bot :
∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.zmultiples g = ⊥ ↔ g = 0
This theorem states that for any additive group `G` and any element `g` of `G`, the subgroup generated by `g` (i.e., the set of all integer multiples of `g`) is trivial (consists only of the additive identity, denoted by `⊥`) if and only if `g` itself is the additive identity (0). In other words, an element generates a trivial subgroup if and only if it is zero.
More concisely: An element `g` in an additive group generates a trivial subgroup if and only if `g = 0`.
|
AddSubgroup.zmultiples_le_of_mem
theorem AddSubgroup.zmultiples_le_of_mem :
∀ {G : Type u_1} [inst : AddGroup G] {g : G} {H : AddSubgroup G}, g ∈ H → AddSubgroup.zmultiples g ≤ H
This theorem, referred to as an alias of the reverse direction of `AddSubgroup.zmultiples_le`, states that for any type `G` that has an additive group structure, given any element `g` of `G` and any additive subgroup `H` of `G`, if `g` is an element of `H`, then the subgroup generated by `g` (obtained using `AddSubgroup.zmultiples g`) is a subset of or equal to (`≤`) the subgroup `H`.
More concisely: For any additive group `G`, if `g` is an element of an additive subgroup `H` of `G`, then the subgroup generated by `g` is contained in `H` (i.e., `AddSubgroup.zmultiples g ≤ H`).
|
Subgroup.zpowers_le
theorem Subgroup.zpowers_le :
∀ {G : Type u_1} [inst : Group G] {g : G} {H : Subgroup G}, Subgroup.zpowers g ≤ H ↔ g ∈ H
This theorem states that for any group `G`, any element `g` of `G`, and any subgroup `H` of `G`, the subgroup generated by `g` is a subset of `H` if and only if `g` itself is an element of `H`. In other words, all powers of `g` are in `H` exactly when `g` is in `H`.
More concisely: The subgroup generated by an element `g` in a group `G` is contained in a subgroup `H` if and only if `g` is an element of `H`.
|
Subgroup.zpowers_eq_bot
theorem Subgroup.zpowers_eq_bot : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.zpowers g = ⊥ ↔ g = 1
This theorem states that for any group `G` and any element `g` of `G`, the subgroup generated by `g` (denoted by `Subgroup.zpowers g`) is the trivial subgroup (denoted by `⊥`) if and only if `g` is the identity element of the group (`g = 1`). In other words, the subgroup generated by an element in a group is trivial if and only if that element is the identity element.
More concisely: The subgroup generated by an element in a group is the trivial subgroup if and only if that element is the identity.
|
AddSubgroup.zsmul_mem_zmultiples
theorem AddSubgroup.zsmul_mem_zmultiples :
∀ {G : Type u_1} [inst : AddGroup G] (g : G) (k : ℤ), k • g ∈ AddSubgroup.zmultiples g
The theorem `AddSubgroup.zsmul_mem_zmultiples` states that for any additive group `G` and any element `g` in `G` and any integer `k`, the result of scaling `g` by `k` (i.e., `k • g`) is an element of the subgroup generated by `g`. In other words, it states that any integer multiple of an element `g` of an additive group `G` remains within the subgroup generated by `g`.
More concisely: For any additive group G, integer k, and element g in G, k • g is an element of the subgroup generated by g.
|
AddSubgroup.zmultiples_eq_closure
theorem AddSubgroup.zmultiples_eq_closure :
∀ {G : Type u_1} [inst : AddGroup G] (g : G), AddSubgroup.zmultiples g = AddSubgroup.closure {g}
This theorem states that for any given type `G` which forms an additive group, the subgroup generated by multiples of any element `g` of the group (denoted by `AddSubgroup.zmultiples g`) is equivalent to the closure of the set containing just the element `g` (denoted by `AddSubgroup.closure {g}`). In other words, the cyclic subgroup generated by `g` is the smallest subgroup of `G` that contains `g`.
More concisely: For any additive group `G` and element `g` in `G`, the subgroup generated by multiples of `g` (`AddSubgroup.zmultiples g`) equals the closure of the set containing just `g` (`AddSubgroup.closure {g}`). Alternatively, the cyclic subgroup generated by `g` is the smallest subgroup containing `g`.
|
AddSubgroup.zmultiples_le
theorem AddSubgroup.zmultiples_le :
∀ {G : Type u_1} [inst : AddGroup G] {g : G} {H : AddSubgroup G}, AddSubgroup.zmultiples g ≤ H ↔ g ∈ H
The theorem `AddSubgroup.zmultiples_le` states that for any type `G` with an additive group structure (denoted by `AddGroup G`), a particular element `g` of `G`, and a subgroup `H` of `G`, the subgroup generated by `g` (denoted by `AddSubgroup.zmultiples g`) is a subset of `H` if and only if `g` is an element of `H`. This essentially says that the only way for a subgroup generated by a single element to be contained within a larger subgroup is if that original element is already in the larger subgroup.
More concisely: For any additive group (G, +), element g in G, and subgroup H of G, the subgroup generated by g (AddSubgroup.zmultiples g) is contained in H if and only if g is an element of H.
|