# Documentation

Mathlib.GroupTheory.SpecificGroups.Dihedral

# 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

The group structure on DihedralGroup n.

@[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.

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 / Nat.gcd n ()

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 | => { val := , property := (_ : DihedralGroup.sr (i + 0) = DihedralGroup.sr (i - 0)) } | Sum.inr () => { val := , property := (_ : DihedralGroup.sr (j - 0) = DihedralGroup.sr (j + 0)) } | Sum.inr (Sum.inr ()) => { val := (DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k), DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k)), property := (_ : (DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k), DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k)).fst * (DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k), DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k)).snd = (DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k), DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k)).fst * (DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k), DihedralGroup.sr ((ZMod.unitOfCoprime 2 (_ : ))⁻¹ * k)).snd) } | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := , property := (_ : DihedralGroup.r (i + j) = DihedralGroup.r (j + i)) }
@[simp]
theorem DihedralGroup.OddCommuteEquiv_apply {n : } (hn : Odd n) :
∀ (x : { p // Commute p.fst p.snd }), = match x with | { val := , property := property } => | { val := , property := property } => Sum.inr () | { val := , property := property } => Sum.inr (Sum.inr (Sum.inl (i + j))) | { val := , property := property } => Sum.inr (Sum.inr (Sum.inr (i, j)))
def DihedralGroup.OddCommuteEquiv {n : } (hn : Odd n) :
{ p // Commute p.fst p.snd } 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.

Instances For
theorem DihedralGroup.card_commute_odd {n : } (hn : Odd n) :
Nat.card { p // Commute p.fst p.snd } = 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