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.

r {n : ℕ} : ZMod n → DihedralGroup n
sr {n : ℕ} : ZMod n → DihedralGroup n

Instances For

def instDecidableEqDihedralGroup.decEq {n✝ : ℕ} (x✝ x✝¹ : DihedralGroup n✝) :

Decidable (x✝ = x✝¹)

Equations

instDecidableEqDihedralGroup.decEq (DihedralGroup.r a) (DihedralGroup.r b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
instDecidableEqDihedralGroup.decEq (DihedralGroup.r a) (DihedralGroup.sr a_1) = isFalse ⋯
instDecidableEqDihedralGroup.decEq (DihedralGroup.sr a) (DihedralGroup.r a_1) = isFalse ⋯
instDecidableEqDihedralGroup.decEq (DihedralGroup.sr a) (DihedralGroup.sr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

instance instDecidableEqDihedralGroup {n✝ : ℕ} :

DecidableEq (DihedralGroup n✝)

Equations

instDecidableEqDihedralGroup = instDecidableEqDihedralGroup.decEq

instance DihedralGroup.instInhabited {n : ℕ} :

Inhabited (DihedralGroup n)

Equations

DihedralGroup.instInhabited = { default := DihedralGroup.one✝ }

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.

@[simp]

theorem DihedralGroup.r_mul_r {n : ℕ} (i j : ZMod n) :

r i * r j = r (i + j)

@[simp]

theorem DihedralGroup.r_mul_sr {n : ℕ} (i j : ZMod n) :

r i * sr j = sr (j - i)

@[simp]

theorem DihedralGroup.sr_mul_r {n : ℕ} (i j : ZMod n) :

sr i * r j = sr (i + j)

@[simp]

theorem DihedralGroup.sr_mul_sr {n : ℕ} (i j : ZMod n) :

sr i * sr j = r (j - i)

@[simp]

theorem DihedralGroup.inv_r {n : ℕ} (i : ZMod n) :

(r i)⁻¹ = r (-i)

@[simp]

theorem DihedralGroup.inv_sr {n : ℕ} (i : ZMod n) :

(sr i)⁻¹ = sr i

@[simp]

theorem DihedralGroup.r_zero {n : ℕ} :

r 0 = 1

theorem DihedralGroup.one_def {n : ℕ} :

1 = r 0

@[simp]

theorem DihedralGroup.r_pow {n : ℕ} (i : ZMod n) (k : ℕ) :

r i ^ k = r (i * ↑k)

@[simp]

theorem DihedralGroup.r_zpow {n : ℕ} (i : ZMod n) (k : ℤ) :

r i ^ k = r (i * ↑k)

instance DihedralGroup.instFintypeOfNeZeroNat {n : ℕ} [NeZero n] :

Fintype (DihedralGroup n)

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

Equations

DihedralGroup.instFintypeOfNeZeroNat = Fintype.ofEquiv (ZMod n ⊕ ZMod n) DihedralGroup.fintypeHelper✝

instance DihedralGroup.instInfiniteOfNatNat :

Infinite (DihedralGroup 0)

instance DihedralGroup.instNontrivial {n : ℕ} :

Nontrivial (DihedralGroup n)

theorem DihedralGroup.card {n : ℕ} [NeZero n] :

Fintype.card (DihedralGroup n) = 2 * n

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

theorem DihedralGroup.nat_card {n : ℕ} :

Nat.card (DihedralGroup n) = 2 * n

theorem DihedralGroup.r_one_pow {n : ℕ} (k : ℕ) :

r 1 ^ k = r ↑k

theorem DihedralGroup.r_one_zpow {n : ℕ} (k : ℤ) :

r 1 ^ k = r ↑k

theorem DihedralGroup.r_one_pow_n {n : ℕ} :

r 1 ^ n = 1

theorem DihedralGroup.sr_mul_self {n : ℕ} (i : ZMod n) :

sr i * sr i = 1

@[simp]

theorem DihedralGroup.orderOf_sr {n : ℕ} (i : ZMod n) :

orderOf (sr i) = 2

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

@[simp]

theorem DihedralGroup.orderOf_r_one {n : ℕ} :

orderOf (r 1) = n

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

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.

theorem DihedralGroup.exponent {n : ℕ} :

Monoid.exponent (DihedralGroup n) = lcm n 2

theorem DihedralGroup.not_commutative {n : ℕ} :

n ≠ 1 → n ≠ 2 → ¬Std.Commutative fun (x y : DihedralGroup n) => x * y

theorem DihedralGroup.commutative_iff {n : ℕ} :

(Std.Commutative fun (x y : DihedralGroup n) => x * y) ↔ n = 1 ∨ n = 2

theorem DihedralGroup.not_isCyclic {n : ℕ} (h1 : n ≠ 1) :

¬IsCyclic (DihedralGroup n)

theorem DihedralGroup.isCyclic_iff {n : ℕ} :

IsCyclic (DihedralGroup n) ↔ n = 1

instance DihedralGroup.instIsKleinFourOfNatNat :

IsKleinFour (DihedralGroup 2)

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

@[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), ⋯⟩

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

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

@DihedralGroup.OddCommuteEquiv = @DihedralGroup.oddCommuteEquiv

Instances For

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

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

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.

theorem DihedralGroup.card_conjClasses_odd {n : ℕ} (hn : Odd n) :

Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2