toInteger_isPrimitiveRoot — Mathlib

English

If ζ is a primitive p-th root of unity in a cyclotomic extension with p prime, then its image hζ.toInteger is also a primitive root of order p.

Русский

Если ζ — примитивный p-й корень единства в циклотомическом расширении, то образ hζ.toInteger также является примитивным корнем порядка p.

LaTeX

$$$$ \text{IsPrimitiveRoot}(h\zeta^{\mathrm{toInteger}}, p) $$$$

Lean4

theorem toInteger_isPrimitiveRoot {k : ℕ} [NeZero k] (hζ : IsPrimitiveRoot ζ k) : IsPrimitiveRoot hζ.toInteger k :=
  IsPrimitiveRoot.of_map_of_injective (by exact hζ) RingOfIntegers.coe_injective

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