normalizedFactors_cyclotomic_card

English

Let p be prime and p ∤ n. If a polynomial P over the ring ZMod p divides cyclotomic n (ZMod p), and deg P equals the order of the unit modulo n, then P is irreducible.

Русский

Пусть p — простое и p не делит n. Если P делит cyclotomic n в ZMod p и deg P равен порядку единицы по модулю n, то P неразложим.

LaTeX

$$$$ P \\mid \\operatorname{cyclotomic}(n, \\mathbb{Z}/p\\mathbb{Z}) \\wedge \\deg P = \\operatorname{orderOf}(\\text{unitOfCoprime}(_ , p)) \\Rightarrow P \\text{ irreducible}. $$$$

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. This result computes the
  number of distinct irreducible factors of `cyclotomic n K`. -/
theorem normalizedFactors_cyclotomic_card :
    (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime _ (hn.pow_left f)) :=
  by
  have h := prod_normalizedFactors (cyclotomic_ne_zero n K)
  have : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) := fun P hP ↦
    natDegree_of_mem_normalizedFactors_cyclotomic hK hn hP
  have H := natDegree_eq_of_degree_eq <| degree_eq_degree_of_associated h
  rw [natDegree_cyclotomic, natDegree_multiset_prod _ (zero_notMem_normalizedFactors _), map_congr rfl this] at H
  simp only [map_const', sum_replicate, smul_eq_mul] at H
  rw [← H, mul_div_left _ (orderOf_pos _), toFinset_card_of_nodup]
  refine nodup_iff_count_le_one.mpr (fun P ↦ ?_)
  by_contra! H
  have : NeZero (n : K) := by
    refine ⟨fun H ↦ ?_⟩
    have := charP_of_card_eq_prime_pow hK
    exact
      hp.out.coprime_iff_not_dvd.mp ((coprime_pow_left_iff (pos_of_ne_zero <| f_ne_zero hK) _ _).mp (hn.pow_left f))
        ((CharP.cast_eq_zero_iff K p _).mp H)
  have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by omega)
  refine (prime_of_normalized_factor _ hP).not_unit (squarefree_cyclotomic n K P ?_)
  have : { P, P } ≤ normalizedFactors (cyclotomic n K) :=
    by
    refine le_iff_count.mpr (fun Q ↦ ?_)
    by_cases hQ : Q = P
    · simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton, count_eq_one_of_mem, reduceAdd]
      cutsat
    · simp [hQ]
  have := prod_dvd_prod_of_le this
  simp only [insert_eq_cons, prod_cons, prod_singleton] at this
  exact this.trans h.dvd

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