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.

source
inductive DihedralGroup (n : ℕ) :
Type

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
    source
    instance instDecidableEqDihedralGroup {n✝ : ℕ} :
    DecidableEq (DihedralGroup n✝)
    Equations
    source
    instance DihedralGroup.instInhabited {n : ℕ} :
    Inhabited (DihedralGroup n)
    Equations
    source
    instance DihedralGroup.instGroup {n : ℕ} :
    Group (DihedralGroup n)

    The group structure on DihedralGroup n.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem DihedralGroup.r_mul_r {n : ℕ} (i j : ZMod n) :
    r i * r j = r (i + j)
    source
    @[simp]
    theorem DihedralGroup.r_mul_sr {n : ℕ} (i j : ZMod n) :
    r i * sr j = sr (j - i)
    source
    @[simp]
    theorem DihedralGroup.sr_mul_r {n : ℕ} (i j : ZMod n) :
    sr i * r j = sr (i + j)
    source
    @[simp]
    theorem DihedralGroup.sr_mul_sr {n : ℕ} (i j : ZMod n) :
    sr i * sr j = r (j - i)
    source
    @[simp]
    theorem DihedralGroup.inv_r {n : ℕ} (i : ZMod n) :
    (r i)⁻¹ = r (-i)
    source
    @[simp]
    theorem DihedralGroup.inv_sr {n : ℕ} (i : ZMod n) :
    (sr i)⁻¹ = sr i
    source
    @[simp]
    theorem DihedralGroup.r_zero {n : ℕ} :
    r 0 = 1
    source
    theorem DihedralGroup.one_def {n : ℕ} :
    1 = r 0
    source
    @[simp]
    theorem DihedralGroup.r_pow {n : ℕ} (i : ZMod n) (k : ℕ) :
    r i ^ k = r (i * ↑k)
    source
    @[simp]
    theorem DihedralGroup.r_zpow {n : ℕ} (i : ZMod n) (k : ℤ) :
    r i ^ k = r (i * ↑k)
    source
    instance DihedralGroup.instFintypeOfNeZeroNat {n : ℕ} [NeZero n] :
    Fintype (DihedralGroup n)

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

    Equations
    source
    instance DihedralGroup.instInfiniteOfNatNat :
    Infinite (DihedralGroup 0)
    source
    instance DihedralGroup.instNontrivial {n : ℕ} :
    Nontrivial (DihedralGroup n)
    source
    theorem DihedralGroup.card {n : ℕ} [NeZero n] :
    Fintype.card (DihedralGroup n) = 2 * n

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

    source
    theorem DihedralGroup.nat_card {n : ℕ} :
    Nat.card (DihedralGroup n) = 2 * n
    source
    theorem DihedralGroup.r_one_pow {n : ℕ} (k : ℕ) :
    r 1 ^ k = r ↑k
    source
    theorem DihedralGroup.r_one_zpow {n : ℕ} (k : ℤ) :
    r 1 ^ k = r ↑k
    source
    theorem DihedralGroup.r_one_pow_n {n : ℕ} :
    r 1 ^ n = 1
    source
    theorem DihedralGroup.sr_mul_self {n : ℕ} (i : ZMod n) :
    sr i * sr i = 1
    source
    @[simp]
    theorem DihedralGroup.orderOf_sr {n : ℕ} (i : ZMod n) :
    orderOf (sr i) = 2

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

    source
    @[simp]
    theorem DihedralGroup.orderOf_r_one {n : ℕ} :
    orderOf (r 1) = n

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

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

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

    source
    theorem DihedralGroup.exponent {n : ℕ} :
    Monoid.exponent (DihedralGroup n) = lcm n 2
    source
    theorem DihedralGroup.not_commutative {n : ℕ} :
    n ≠ 1 → n ≠ 2 → ¬Std.Commutative fun (x y : DihedralGroup n) => x * y
    source
    theorem DihedralGroup.commutative_iff {n : ℕ} :
    (Std.Commutative fun (x y : DihedralGroup n) => x * y) ↔ n = 1 ∨ n = 2
    source
    theorem DihedralGroup.not_isCyclic {n : ℕ} (h1 : n ≠ 1) :
    ¬IsCyclic (DihedralGroup n)
    source
    theorem DihedralGroup.isCyclic_iff {n : ℕ} :
    IsCyclic (DihedralGroup n) ↔ n = 1
    source
    def DihedralGroup.oddCommuteEquiv {n : ℕ} (hn : Odd n) :
    { p : DihedralGroup n × DihedralGroup n // 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
      source
      @[simp]
      theorem DihedralGroup.oddCommuteEquiv_symm_apply {n : ℕ} (hn : Odd n) (x✝ : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) :
      (oddCommuteEquiv hn).symm x✝ = match x✝ with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩
      source
      @[simp]
      theorem DihedralGroup.oddCommuteEquiv_apply {n : ℕ} (hn : Odd n) (x✝ : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) :
      (oddCommuteEquiv hn) x✝ = match x✝ with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))
      source
      @[deprecated DihedralGroup.oddCommuteEquiv (since := "2025-05-07")]
      def DihedralGroup.OddCommuteEquiv {n : ℕ} (hn : Odd n) :
      { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } ≃ ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n

      Alias of DihedralGroup.oddCommuteEquiv.

      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
      Instances For
        source
        @[deprecated DihedralGroup.oddCommuteEquiv_apply (since := "2025-05-07")]
        theorem DihedralGroup.OddCommuteEquiv_apply {n : ℕ} (hn : Odd n) (x✝ : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) :
        (oddCommuteEquiv hn) x✝ = match x✝ with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))

        Alias of DihedralGroup.oddCommuteEquiv_apply.

        source
        @[deprecated DihedralGroup.oddCommuteEquiv_symm_apply (since := "2025-05-07")]
        theorem DihedralGroup.OddCommuteEquiv_symm_apply {n : ℕ} (hn : Odd n) (x✝ : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) :
        (oddCommuteEquiv hn).symm x✝ = match x✝ with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩

        Alias of DihedralGroup.oddCommuteEquiv_symm_apply.

        source
        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.

        source
        theorem DihedralGroup.card_conjClasses_odd {n : ℕ} (hn : Odd n) :
        Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2