English
Let K be a finite field with cardinality p^f and let P be an irreducible factor of the n-th cyclotomic polynomial over K, with gcd(p, n) = 1. Then the degree of P equals the multiplicative order of p^f modulo n.
Русский
Пусть K — конечное поле с кардинальностью p^f и P — неприводимый множитель n-ой циклотоми над K, при этом gcd(p, n) = 1. Тогда deg P равен мультипликатному порядку p^f по модулю n.
LaTeX
$$$$ \\deg P = \\operatorname{orderOf}(p^f \\bmod n). $$$$
Lean4
/-- Let `K` be a finite field of cardinality `p ^ f` and let `P` be an irreducible factor of the
`n`-th cyclotomic polynomial over `K`, where `p` and `n` are coprime. Then the degree of `P` is
the multiplicative order of `p ^ f` modulo `n`. -/
theorem natDegree_of_dvd_cyclotomic_of_irreducible (hP : P ∣ cyclotomic n K) (hPirr : Irreducible P) :
P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) :=
by
obtain ⟨A, hA⟩ := hP
have hQ : P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K :=
by
refine ⟨A * C P.leadingCoeff, ?_⟩
calc
_ = P * A := hA
_ = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A := by simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]
_ = _ := by ring
simpa [← natDegree_mul_leadingCoeff_self_inv P] using
natDegree_of_dvd_cyclotomic_of_irreducible_of_monic hK hn hQ (irreducible_mul_leadingCoeff_inv.mpr hPirr)
(monic_mul_leadingCoeff_inv hPirr.ne_zero)
