zpow_eq_one

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

URI: https://scilib.ai/kg/mathlib#IsPrimitiveRoot.zpow_eq_one

English

Let ζ be a primitive k-th root of unity. Then ζ^k = 1.

Русский

Пусть ζ — примитивный корень k-й степени единицы. Тогда ζ^k = 1.

LaTeX

$$$IsPrimitiveRoot(\\zeta, k) \\Rightarrow \\zeta^k = 1$$$

Lean4

theorem zpow_eq_one (h : IsPrimitiveRoot ζ k) : ζ ^ (k : ℤ) = 1 := by exact_mod_cast h.pow_eq_one

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

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

Разделы

Аффилиация

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