English
Let K be a finite field with q = p^f elements and gcd(p, n) = 1. For any P in the normalized factors of cyclotomic n over K, the natDegree of P equals the order of p^f modulo n.
Русский
Пусть K — конечное поле с q = p^f элементами и gcd(p, n) = 1. Для любого P в нормализованных факторах cyclotomic n над K deg P равно порядку p^f по модулю n.
LaTeX
$$$$ P \\in \\operatorname{normalizedFactors}(\\operatorname{cyclotomic}(n, K)) \\Rightarrow P\\text{ natDegree }= \\operatorname{orderOf}(p^f). $$$$
Lean4
theorem _root_.isRoot_of_unity_iff (h : 0 < n) (R : Type*) [CommRing R] [IsDomain R] {ζ : R} :
ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ := by
rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ← prod_cyclotomic_eq_X_pow_sub_one h,
isRoot_prod]
