Nat.card_zmultiples
theorem Nat.card_zmultiples :
∀ {α : Type u_3} [inst : AddGroup α] (a : α), Nat.card ↥(AddSubgroup.zmultiples a) = addOrderOf a
The theorem `Nat.card_zmultiples` states that for any additively group-structured type `α` and any element `a` of `α`, the cardinality of the subgroup generated by `a` is equal to the additive order of `a`. In mathematical terms, this means that the number of distinct elements obtained by repeatedly adding `a` to itself (including the zero element) is equal to the least positive integer `n` such that adding `a` to itself `n` times yields the zero element. If no such `n` exists (i.e., `a` is of infinite order), both the cardinality of the subgroup and the additive order are defined to be zero.
More concisely: The cardinality of the subgroup generated by an element `a` in an additively group-structured type `α` equals the additive order of `a`.
|
IsOfFinOrder.finite_zpowers
theorem IsOfFinOrder.finite_zpowers :
∀ {α : Type u_3} [inst : Group α] {a : α}, IsOfFinOrder a → (↑(Subgroup.zpowers a)).Finite
This is a theorem stating that for any group `α` and any element `a` of this group, if `a` has finite order (i.e., there exists a positive integer `n` such that `a` raised to the power `n` equals the identity element of the group), then the subgroup of `α` generated by `a` (the set of all powers of `a`) is finite. In other words, if an element of a group is of finite order, then the set of all its powers also has a finite number of elements.
More concisely: Given a group `α` and an element `a` of finite order `n` in `α`, the subgroup generated by `a` consists of `n` elements.
|
Nat.card_zpowers
theorem Nat.card_zpowers : ∀ {α : Type u_3} [inst : Group α] (a : α), Nat.card ↥(Subgroup.zpowers a) = orderOf a := by
sorry
The theorem `Nat.card_zpowers` states that for any group `α` and any element `a` of this group, the cardinality of the subgroup generated by `a` (obtained using the `Subgroup.zpowers` function on `a`) is equal to the order of the element `a` (obtained using the `orderOf` function). In other words, the number of distinct elements in the subgroup generated by an element is the same as the order of that element. The order of an element is the smallest positive integer `n` such that raising the element to the power `n` gives the identity of the group. If such an `n` does not exist (the element has infinite order), both the cardinality of the subgroup and the order of the element are defined to be `0`.
More concisely: The cardinality of the subgroup generated by an element in a group equals the order of that element.
|