minpoly_dvd_x_pow_sub_one — Mathlib

English

The minimal polynomial of a primitive root μ over ℤ divides X^n - 1.

Русский

Минимальный многочлен μ над ℤ делится на X^n - 1.

LaTeX

$$minpoly ℤ μ ∣ X^n - 1$$

Lean4

/-- The minimal polynomial of a root of unity `μ` divides `X ^ n - 1`. -/
theorem minpoly_dvd_x_pow_sub_one : minpoly ℤ μ ∣ X ^ n - 1 :=
  by
  rcases n.eq_zero_or_pos with (rfl | h0)
  · simp
  apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
  simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, aeval_one, map_sub, sub_self]

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