inv — Mathlib

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

Похожие утверждения