QuaternionGroup.quaternionGroup_one_isCyclic
theorem QuaternionGroup.quaternionGroup_one_isCyclic : IsCyclic (QuaternionGroup 1)
This theorem states that in the specific case where n equals 1, the Quaternion Group of 1 is a cyclic group with an order of 4. In other words, the group operation can be generated by repeatedly applying a single element, and there are four unique elements in that group.
More concisely: The Quaternion Group of order 1 is a cyclic group of order 4.
|
QuaternionGroup.card
theorem QuaternionGroup.card : ∀ {n : ℕ} [inst : NeZero n], Fintype.card (QuaternionGroup n) = 4 * n
This theorem states that if `n` is a positive natural number (i.e., `n` is not zero), then the cardinality (or the number of elements) of the `QuaternionGroup n` is `4n`. In other words, for any positive natural number `n`, the Quaternion Group of order `n` contains `4n` elements.
More concisely: The Quaternion Group of order `n` has `4n` elements for any positive natural number `n`.
|
QuaternionGroup.orderOf_a_one
theorem QuaternionGroup.orderOf_a_one : ∀ {n : ℕ}, orderOf (QuaternionGroup.a 1) = 2 * n
The theorem `QuaternionGroup.orderOf_a_one` states that for any natural number `n` where `n` is greater than `0`, the order of the element `QuaternionGroup.a 1` is `2 * n`. In group theory, the order of an element is the smallest positive integer `n` such that `x ^ n = 1`. In the special case of the quaternion group, this theorem asserts that the order of `QuaternionGroup.a 1` is exactly twice the given natural number.
More concisely: The order of the quaternion `QuaternionGroup.a 1` is twice the given natural number `n` for `n > 0`.
|
QuaternionGroup.orderOf_a
theorem QuaternionGroup.orderOf_a :
∀ {n : ℕ} [inst : NeZero n] (i : ZMod (2 * n)), orderOf (QuaternionGroup.a i) = 2 * n / (2 * n).gcd i.val := by
sorry
This theorem states that for any natural number 'n' which is greater than zero, and any integer modulo '2n' (represented as 'i'), the order of the element 'a i' in the Quaternion Group is equal to '2n' divided by the greatest common divisor of '2n' and the value of 'i'. The order of an element in a group is the smallest positive integer 'n' for which the element raised to the 'n'-th power equals the identity of the group. If no such 'n' exists, the order is conventionally defined as zero.
More concisely: For any quaternion group element a of order 2n and integer i modulo 2n, the order of ai is given by 2n divided by the greatest common divisor of 2n and i.
|
QuaternionGroup.a_one_pow
theorem QuaternionGroup.a_one_pow : ∀ {n : ℕ} (k : ℕ), QuaternionGroup.a 1 ^ k = QuaternionGroup.a ↑k
This theorem states that for any natural number `n` and `k`, the quaternion group element `a` raised to the power of `k` when its input parameter is `1`, is actually the same as the quaternion group element `a` when its input parameter is the natural number `k`. The `QuaternionGroup.a 1 ^ k` expression represents the quaternion group operation repeated `k` times on the element `a` with input `1`, and the theorem asserts this is equal to the quaternion group element `a` with input `k`.
More concisely: For any quaternion group element `a` and natural number `k`, `QuaternionGroup.a ^ k = QuaternionGroup.a 1 ^ k`.
|
QuaternionGroup.orderOf_xa
theorem QuaternionGroup.orderOf_xa :
∀ {n : ℕ} [inst : NeZero n] (i : ZMod (2 * n)), orderOf (QuaternionGroup.xa i) = 4
The theorem `QuaternionGroup.orderOf_xa` states that for any natural number `n` that is non-zero, and for any integer `i` modulo `2n` (denoted as `ZMod (2 * n)`), the order of the element `QuaternionGroup.xa i` is 4. In mathematical terms, this means that if you multiply `QuaternionGroup.xa i` by itself 4 times, you will get the identity element, and 4 is the smallest such positive integer.
More concisely: For any integer `i` modulo `2n` in the Quaternion Group, the order of the element `QuaternionGroup.xa i` is 4.
|