# Dihedral Groups #

We define the dihedral groups DihedralGroup n, with elements r i and sr i for i : ZMod n.

For n ≠ 0, DihedralGroup n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. DihedralGroup 0 corresponds to the infinite dihedral group.

inductive DihedralGroup (n : ) :

For n ≠ 0, DihedralGroup n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. DihedralGroup 0 corresponds to the infinite dihedral group.

Instances For
instance instDecidableEqDihedralGroup :
{n : } →
Equations
• instDecidableEqDihedralGroup = decEqDihedralGroup✝
Equations
• DihedralGroup.instInhabited = { default := DihedralGroup.one }
instance DihedralGroup.instGroup {n : } :

The group structure on DihedralGroup n.

Equations
• DihedralGroup.instGroup =
@[simp]
theorem DihedralGroup.r_mul_r {n : } (i : ZMod n) (j : ZMod n) :
@[simp]
theorem DihedralGroup.r_mul_sr {n : } (i : ZMod n) (j : ZMod n) :
@[simp]
theorem DihedralGroup.sr_mul_r {n : } (i : ZMod n) (j : ZMod n) :
@[simp]
theorem DihedralGroup.sr_mul_sr {n : } (i : ZMod n) (j : ZMod n) :

If 0 < n, then DihedralGroup n is a finite group.

Equations
Equations
• =
theorem DihedralGroup.card {n : } [] :
= 2 * n

If 0 < n, then DihedralGroup n has 2n elements.

theorem DihedralGroup.nat_card {n : } :
= 2 * n
@[simp]
theorem DihedralGroup.r_one_pow {n : } (k : ) :
=
theorem DihedralGroup.sr_mul_self {n : } (i : ZMod n) :
@[simp]
theorem DihedralGroup.orderOf_sr {n : } (i : ZMod n) :
= 2

If 0 < n, then sr i has order 2.

@[simp]

If 0 < n, then r 1 has order n.

theorem DihedralGroup.orderOf_r {n : } [] (i : ZMod n) :
= n / n.gcd i.val

If 0 < n, then i : ZMod n has order n / gcd n i.

@[simp]
theorem DihedralGroup.OddCommuteEquiv_symm_apply {n : } (hn : Odd n) :
∀ (x : ZMod n ZMod n ZMod n ZMod n × ZMod n), .symm x = match x with | => , | Sum.inr (Sum.inl j) => , | Sum.inr (Sum.inr (Sum.inl k)) => (DihedralGroup.sr (⁻¹ * k), DihedralGroup.sr (⁻¹ * k)), | Sum.inr (Sum.inr (Sum.inr (i, j))) => ,
@[simp]
theorem DihedralGroup.OddCommuteEquiv_apply {n : } (hn : Odd n) :
∀ (x : { p : // Commute p.1 p.2 }), = match x with | , property => | , property => Sum.inr (Sum.inl j) | , property => Sum.inr (Sum.inr (Sum.inl (i + j))) | , property => Sum.inr (Sum.inr (Sum.inr (i, j)))
def DihedralGroup.OddCommuteEquiv {n : } (hn : Odd n) :
{ p : // Commute p.1 p.2 } ZMod n ZMod n ZMod n ZMod n × ZMod n

If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs (represented as $n + n + n + n*n$) of commuting elements.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem DihedralGroup.card_commute_odd {n : } (hn : Odd n) :
Nat.card { p : // Commute p.1 p.2 } = n * (n + 3)

If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs of commuting elements.

theorem DihedralGroup.card_conjClasses_odd {n : } (hn : Odd n) :
= (n + 3) / 2