English
For every n and a ∈ Z/nZ, the map dihedralAct(n) a is an involution; applying it twice yields the identity on Z/nZ.
Русский
Для любого n и любого a ∈ Z/nZ отображение dihedralAct(n) a является инволюцией: применение дважды даёт тождественное отображение.
LaTeX
$$$\forall n, a:\ (\mathrm{dihedralAct}_n(a))^{2} = \mathrm{id}_{\mathbb{Z}/n\mathbb{Z}}.$$$
Lean4
theorem inv (n : ℕ) (a : ZMod n) : Function.Involutive (dihedralAct n a) :=
by
intro b
dsimp only [dihedralAct]
simp