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
    Equations
    • instDecidableEqDihedralGroup = decEqDihedralGroup✝
    Equations
    • DihedralGroup.instInhabited = { default := DihedralGroup.one }

    The group structure on DihedralGroup n.

    Equations
    @[simp]

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

    Equations

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

    @[simp]

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

    @[simp]

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

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

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

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

    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 : DihedralGroup n × DihedralGroup n // 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.