English
For every n, the Dihedral quandle together with the operation a ◃ b := dihedralAct(n)(a)(b) satisfies the quandle axioms (closure, idempotence, and right-invertibility/distributivity).
Русский
Для каждого n диэдральный куандл с операцией a ◃ b = dihedralAct(n)(a)(b) удовлетворяет аксиомам куандла (замкнутость, инволюционная идентичность и правая инвертируемость/распределительность).
LaTeX
$$$\text{Quandle}(\mathrm{Dihedral}(n)) \text{ is a quandle with } a \triangleleft b = \mathrm{dihedralAct}_n(a)(b).$$$
Lean4
instance (n : ℕ) : Quandle (Dihedral n) where
act := dihedralAct n
self_distrib := by
intro x y z
simp only [dihedralAct]
ring_nf
invAct := dihedralAct n
left_inv x := (dihedralAct.inv n x).leftInverse
right_inv x := (dihedralAct.inv n x).rightInverse
fix := by
intro x
simp only [dihedralAct]
ring_nf
