orderOf_five

Mathlib.RingTheory.ZMod.UnitsCyclic

URI: https://scilib.ai/kg/mathlib#ZMod.orderOf_five

English

For any n, the order of 5 in (Z/2^{n+2}Z)× equals 2^n.

Русский

Для любого n порядок 5 в (Z/2^{n+2}Z)× равен 2^n.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\operatorname{orderOf}(5 \\\\bmod 2^{n+2}) = 2^{n}.$$$

Lean4

theorem orderOf_five (n : ℕ) : orderOf (5 : ZMod (2 ^ (n + 2))) = 2 ^ n :=
  by
  convert orderOf_one_add_four_mul 1 (by simp) n
  norm_num

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

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

Разделы

Аффилиация

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