pow_of_prime — Mathlib

English

If h is a primitive root ζ of order k and p is prime with p ∤ k, then ζ^p is a primitive root of order k.

Русский

Если h — примитивный корень ζ порядка k и p — простое число такое, что p не делит k, то ζ^p — примитивный корень порядка k.

LaTeX

$$$$\text{If } h: IsPrimitiveRoot(\zeta, k) \text{ and } p \text{ prime with } p \nmid k, \text{ then } IsPrimitiveRoot(\zeta^p, k).$$$$

Lean4

theorem pow_of_prime (h : IsPrimitiveRoot ζ k) {p : ℕ} (hprime : Nat.Prime p) (hdiv : ¬p ∣ k) :
    IsPrimitiveRoot (ζ ^ p) k :=
  h.pow_of_coprime p (hprime.coprime_iff_not_dvd.2 hdiv)

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