inductive AlgebraInLean.Dihedral (n : ℕ) [NeZero n] : Type

The dihedral group Dₙ has 2n elements: the n rotations already in Cₙ, and the reflections of all of these rotations. In particular, an object .rotation k : Dihedral n represents a rotation by 2kπ/n radians, like the elements of Cₙ, and an object .reflection k : Dihedral n represents a reflection (across some particular line) followed by a rotation by 2kπ/n radians.

• rotation: {n : ℕ} → [inst : NeZero n] → Fin n → AlgebraInLean.Dihedral n
• reflection: {n : ℕ} → [inst : NeZero n] → Fin n → AlgebraInLean.Dihedral n

def AlgebraInLean.Dihedral.op {n : ℕ} [NeZero n] : AlgebraInLean.Dihedral n → AlgebraInLean.Dihedral n → AlgebraInLean.Dihedral n

Equations

• One or more equations did not get rendered due to their size.

def AlgebraInLean.Dihedral.inv {n : ℕ} [NeZero n] : AlgebraInLean.Dihedral n → AlgebraInLean.Dihedral n

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraInLean.instGroupDihedral (n : ℕ) [NeZero n] : AlgebraInLean.Group (AlgebraInLean.Dihedral n)

Equations

• AlgebraInLean.instGroupDihedral n = AlgebraInLean.Group.mk AlgebraInLean.Dihedral.inv ⋯

theorem AlgebraInLean.D₃_nonabelian : ¬∀ (a b : AlgebraInLean.Dihedral 3), AlgebraInLean.μ a b = AlgebraInLean.μ b a