totient_le_degree_minpoly — Mathlib

English

The totient φ(n) is at most the degree of the minimal polynomial of μ over ℤ.

Русский

Тотипент φ(n) не превосходит степень минимального полинома μ над ℤ.

LaTeX

$$$\varphi(n) \le (\minpoly_{\mathbb{Z}}(\mu)).\mathrm{natDegree}$$$

Lean4

/-- The degree of the minimal polynomial of `μ` is at least `totient n`. -/
theorem totient_le_degree_minpoly : Nat.totient n ≤ (minpoly ℤ μ).natDegree := by
  classical
  let P : ℤ[X] := minpoly ℤ μ
  let P_K : K[X] := map (Int.castRingHom K) P
  calc
    n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
    _ ≤ P_K.roots.toFinset.card := (Finset.card_le_card (is_roots_of_minpoly h))
    _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
    _ ≤ P_K.natDegree := (card_roots' _)
    _ ≤ P.natDegree := natDegree_map_le

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