DihedralGroup.one_def
theorem DihedralGroup.one_def : ∀ {n : ℕ}, 1 = DihedralGroup.r 0
This theorem states that for all natural numbers 'n', the identity element (1) of the Dihedral Group is defined as the rotation by 0 degrees. The `DihedralGroup.r 0` in the statement represents a rotation by 0 degrees in the Dihedral Group.
More concisely: For all natural numbers n, the identity element in the Dihedral Group is the rotation by 0 degrees. Equivalently, DihedralGroup.r 0 = id.
|
DihedralGroup.orderOf_sr
theorem DihedralGroup.orderOf_sr : ∀ {n : ℕ} (i : ZMod n), orderOf (DihedralGroup.sr i) = 2
The theorem `DihedralGroup.orderOf_sr` states that for any natural number `n` greater than zero, and for any integer modulo `n` (represented by `i : ZMod n`), the order of the symbol rotation operation `sr i` in the dihedral group is always 2. In mathematical terms, this means that applying `sr i` twice will bring the system back to its original state.
More concisely: The order of the symbol rotation operation in the dihedral group is 2 for any integer modulo a positive natural number.
|
DihedralGroup.r_one_pow
theorem DihedralGroup.r_one_pow : ∀ {n : ℕ} (k : ℕ), DihedralGroup.r 1 ^ k = DihedralGroup.r ↑k
This theorem states that for any natural number `n` and any natural number `k`, the rotation operation `r 1` of the Dihedral Group raised to the power `k` is equal to the rotation `r` by `k`. In mathematical terms, it signifies that power operations within the Dihedral Group can be simplified by directly applying the rotation by a given degree.
More concisely: For any natural numbers $n$ and $k$, in the Dihedral Group, $r^k = r$ where $r$ is a rotation operation and $r^k$ denotes raising $r$ to the power of $k$.
|
DihedralGroup.orderOf_r_one
theorem DihedralGroup.orderOf_r_one : ∀ {n : ℕ}, orderOf (DihedralGroup.r 1) = n
This theorem states that for any natural number `n` such that `n` is greater than zero, the order of the element `r 1` of the Dihedral group is equal to `n`. In other words, `r 1` is an element of a Dihedral group which, when multiplied by itself `n` times, results in the identity element of the group.
More concisely: For any positive natural number `n`, the order of the element `r 1` in the Dihedral group is `n`.
|
DihedralGroup.card
theorem DihedralGroup.card : ∀ {n : ℕ} [inst : NeZero n], Fintype.card (DihedralGroup n) = 2 * n
The theorem states that if `n` is a positive natural number (i.e., `n > 0`), then the cardinality (or the number of elements) of the Dihedral Group `DihedralGroup n` is equal to `2n`. In mathematical terms, the Dihedral Group of order `n` has `2n` elements.
More concisely: The Dihedral Group of order `n` has `2 * n` elements.
|
DihedralGroup.card_commute_odd
theorem DihedralGroup.card_commute_odd : ∀ {n : ℕ}, Odd n → Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
The theorem `DihedralGroup.card_commute_odd` states that for any odd natural number `n`, the number of pairs of elements in the Dihedral group of order `2n` that commute (i.e., their multiplication is commutative) is equal to `n*(n+3)`. Here, an element `a` of a semiring is said to be odd if there exists an integer `k` such that `a = 2*k + 1`. Commutativity between two elements `a` and `b` means `a * b = b * a`. The Dihedral group of order `2n` is a mathematical construct used in group theory, a branch of abstract algebra.
More concisely: The number of commuting element pairs in the Dihedral group of order 2n for an odd natural number n is n*(n+3).
|
DihedralGroup.orderOf_r
theorem DihedralGroup.orderOf_r :
∀ {n : ℕ} [inst : NeZero n] (i : ZMod n), orderOf (DihedralGroup.r i) = n / n.gcd i.val
The theorem `DihedralGroup.orderOf_r` states that for any non-zero natural number `n`, the order of an element `i` (which is an integer modulo `n`) in the Dihedral group is equal to the quotient of `n` divided by the greatest common divisor of `n` and the value of `i`. This means that if you repeatedly apply the group operation (denoted by `DihedralGroup.r`) `n / gcd(n, i)` times to `i`, you will get back to the identity element of the group. This result applies to all elements `i` in this particular representation of the Dihedral group.
More concisely: The order of an element `i` in the Dihedral group of order `n` is equal to `n / gcd(n, i)`.
|