orderOf_sr

Mathlib.GroupTheory.SpecificGroups.Dihedral

URI: https://scilib.ai/kg/mathlib#DihedralGroup.orderOf_sr

← MathLib Explorer

English

If 0 < n, then for every i ∈ ZMod n, the element sr(i) has order 2.

Русский

Если 0 < n, то для каждого i ∈ ZMod n элемент sr(i) имеет порядок 2.

LaTeX

$$\operatorname{order}(\mathrm{sr}(i)) = 2$$

Lean4

/-- If `0 < n`, then `sr i` has order 2.
-/
@[simp]
theorem orderOf_sr (i : ZMod n) : orderOf (sr i) = 2 :=
  by
  apply orderOf_eq_prime
  · rw [sq, sr_mul_self]
  · simp [← r_zero]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru