pow_of_dvd — Mathlib

English

If h is a primitive root ζ k and p ≠ 0 divides k, then ζ^p is a primitive root of order k/p.

Русский

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

LaTeX

$$$$\text{If } h: IsPrimitiveRoot(\zeta,k) \text{ and } p \ne 0 \text{ and } p \mid k, \text{ then } IsPrimitiveRoot(\zeta^p, k/p).$$$$

Lean4

theorem pow_of_dvd (h : IsPrimitiveRoot ζ k) {p : ℕ} (hp : p ≠ 0) (hdiv : p ∣ k) : IsPrimitiveRoot (ζ ^ p) (k / p) :=
  by
  rw [h.eq_orderOf] at hdiv ⊢
  rw [← orderOf_pow_of_dvd hp hdiv]
  exact IsPrimitiveRoot.orderOf _

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