pow_isRoot_minpoly — Mathlib

English

For a primitive n-th root μ and any p coprime to n, μ^p is a root of the minimal polynomial of μ.

Русский

Для примитивного μ n-й степени и любого p, взаимно простого с n, μ^p является корнем минимального полинома μ.

LaTeX

$$$\left(\operatorname{map}\left(\operatorname{Int.castRingHom}(K)\right)(\minpoly_{\mathbb{Z}}(\mu))\right)\text{IsRoot}(\mu^{p})$$

Lean4

/-- If `m : ℕ` is coprime with `n`,
then the minimal polynomial of a primitive `n`-th root of unity `μ`
has `μ ^ m` as root. -/
theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.Coprime m n) : IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m) :=
  by
  simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
  exact minpoly.aeval ℤ (μ ^ m)

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