toInteger_cube_eq_one

Mathlib.NumberTheory.Cyclotomic.Three

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

English

For a primitive cube root hζ, its integer image satisfies (hζ.toInteger)^3 = 1.

Русский

Для примитивного кубического корня hζ его целочисленное отображение удовлетворяет (hζ.toInteger)^3 = 1.

LaTeX

$$$\bigl(h_{\zeta}.toInteger\bigr)^{3} = 1$$$

Lean4

theorem _root_.IsPrimitiveRoot.toInteger_cube_eq_one : hζ.toInteger ^ 3 = 1 :=
  hζ.toInteger_isPrimitiveRoot.pow_eq_one

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

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

Разделы

Аффилиация

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