isIntegral — Mathlib

English

If μ is a primitive n-th root with 0 < n, then μ is integral over ℤ.

Русский

Если μ — примитивный n-й корень единицы, и 0 < n, то μ является интегралом над ℤ.

LaTeX

$$isIntegral (h : IsPrimitiveRoot μ n) (hpos : 0 < n) : IsIntegral ℤ μ$$

Lean4

/-- `μ` is integral over `ℤ`. -/
theorem isIntegral (hpos : 0 < n) : IsIntegral ℤ μ :=
  by
  use X ^ n - 1
  constructor
  · exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
  · simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub, sub_self]

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