natDegree_of_mem_normalizedFactors_cyclotomic

English

Let K be a finite field with q = p^f elements and gcd(p, n) = 1. If a polynomial P divides cyclotomic n over K and its degree equals the multiplicative order of p^f modulo n, then P is irreducible.

Русский

Пусть K — конечное поле с q = p^f элементами и gcd(p, n) = 1. Если P делит cyclotomic n над K и deg P равен порядку p^f по модулю n, то P неразложим.

LaTeX

$$$$ P \\mid \\operatorname{cyclotomic}(n, K) \\,\\wedge\\, \\deg P = \\operatorname{orderOf}(p^f) \\Rightarrow P \\text{ irreducible}. $$$$

Lean4

theorem natDegree_of_mem_normalizedFactors_cyclotomic (hP : P ∈ normalizedFactors (cyclotomic n K)) :
    P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) :=
  natDegree_of_dvd_cyclotomic_of_irreducible hK hn (dvd_of_mem_normalizedFactors hP)
    (irreducible_of_normalized_factor P hP)

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