mathlib3 documentation

group_theory.specific_groups.dihedral

Dihedral Groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

For n ≠ 0, dihedral_group 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. dihedral_group 0 corresponds to the infinite dihedral group.

source
@[protected, instance]
def dihedral_group.decidable_eq (n : ℕ) :
decidable_eq (dihedral_group n)
source
inductive dihedral_group (n : ℕ) :
Type

For n ≠ 0, dihedral_group 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. dihedral_group 0 corresponds to the infinite dihedral group.

Instances for dihedral_group
source
@[protected, instance]
def dihedral_group.inhabited {n : ℕ} :
inhabited (dihedral_group n)
Equations
source
@[protected, instance]
def dihedral_group.group {n : ℕ} :
group (dihedral_group n)

The group structure on dihedral_group n.

Equations
  • dihedral_group.group = {mul := mul n, mul_assoc := _, one := one n, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5, npow_zero' := _, npow_succ' := _, inv := inv n, div := div_inv_monoid.div._default mul dihedral_group.group._proof_8 one dihedral_group.group._proof_9 dihedral_group.group._proof_10 (div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5) dihedral_group.group._proof_11 dihedral_group.group._proof_12 inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default mul dihedral_group.group._proof_14 one dihedral_group.group._proof_15 dihedral_group.group._proof_16 (div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5) dihedral_group.group._proof_17 dihedral_group.group._proof_18 inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
source
@[simp]
theorem dihedral_group.r_mul_r {n : ℕ} (i j : zmod n) :
dihedral_group.r i * dihedral_group.r j = dihedral_group.r (i + j)
source
@[simp]
theorem dihedral_group.r_mul_sr {n : ℕ} (i j : zmod n) :
dihedral_group.r i * dihedral_group.sr j = dihedral_group.sr (j - i)
source
@[simp]
theorem dihedral_group.sr_mul_r {n : ℕ} (i j : zmod n) :
dihedral_group.sr i * dihedral_group.r j = dihedral_group.sr (i + j)
source
@[simp]
theorem dihedral_group.sr_mul_sr {n : ℕ} (i j : zmod n) :
dihedral_group.sr i * dihedral_group.sr j = dihedral_group.r (j - i)
source
theorem dihedral_group.one_def {n : ℕ} :
1 = dihedral_group.r 0
source
@[protected, instance]
def dihedral_group.fintype {n : ℕ} [ne_zero n] :
fintype (dihedral_group n)

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

Equations
source
@[protected, instance]
def dihedral_group.nontrivial {n : ℕ} :
nontrivial (dihedral_group n)
source
theorem dihedral_group.card {n : ℕ} [ne_zero n] :
fintype.card (dihedral_group n) = 2 * n

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

source
@[simp]
theorem dihedral_group.r_one_pow {n : ℕ} (k : ℕ) :
dihedral_group.r 1 ^ k = dihedral_group.r ↑k
source
@[simp]
theorem dihedral_group.r_one_pow_n {n : ℕ} :
dihedral_group.r 1 ^ n = 1
source
@[simp]
theorem dihedral_group.sr_mul_self {n : ℕ} (i : zmod n) :
dihedral_group.sr i * dihedral_group.sr i = 1
source
@[simp]
theorem dihedral_group.order_of_sr {n : ℕ} (i : zmod n) :
order_of (dihedral_group.sr i) = 2

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

source
@[simp]
theorem dihedral_group.order_of_r_one {n : ℕ} :
order_of (dihedral_group.r 1) = n

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

source
theorem dihedral_group.order_of_r {n : ℕ} [ne_zero n] (i : zmod n) :
order_of (dihedral_group.r i) = n / n.gcd i.val

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

source
theorem dihedral_group.exponent {n : ℕ} :
monoid.exponent (dihedral_group n) = gcd_monoid.lcm n 2