mathlib documentation

group_theory.dihedral

Dihedral Groups #

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

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

@[instance]
inductive dihedral (n : ) :
Type

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

@[instance]
Equations
@[instance]
def dihedral.group {n : } :

The group structure on dihedral n.

Equations
@[simp]
theorem dihedral.r_mul_r {n : } (i j : zmod n) :
@[simp]
theorem dihedral.r_mul_sr {n : } (i j : zmod n) :
@[simp]
theorem dihedral.sr_mul_r {n : } (i j : zmod n) :
@[simp]
theorem dihedral.sr_mul_sr {n : } (i j : zmod n) :
theorem dihedral.one_def {n : } :
@[instance]
def dihedral.fintype {n : } [fact (0 < n)] :

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

Equations
@[instance]
theorem dihedral.card {n : } [fact (0 < n)] :

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

@[simp]
theorem dihedral.r_one_pow {n : } (k : ) :
@[simp]
theorem dihedral.r_one_pow_n {n : } :
dihedral.r 1 ^ n = 1
@[simp]
theorem dihedral.sr_mul_self {n : } (i : zmod n) :
@[simp]
theorem dihedral.order_of_sr {n : } [fact (0 < n)] (i : zmod n) :

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

@[simp]
theorem dihedral.order_of_r_one {n : } [hnpos : fact (0 < n)] :

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

theorem dihedral.order_of_r {n : } [fact (0 < n)] (i : zmod n) :

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