Real cyclotomic polynomials and 2cos(2πk/n)

TheoremDegree of the real cyclotomic polynomial#●ready to state

For 2 < n, n.totient is even and the natDegree of the real cyclotomic polynomial realCyclotomicPolynomial n equals n.totient / 2. The Even conjunct makes the source's exact half machine-visible under natural-number division.

Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83–90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex

DefinitionReal cyclotomic polynomial#✓fully proved

For a natural number \(n\), the real cyclotomic polynomial \(\psi_n \in \mathbb{Z}[X]\) is the minimal polynomial over \(\mathbb{Z}\) of the complex number \(\zeta + \zeta^{-1}\), where \(\zeta = e^{2\pi i/n}\); for \(n \ge 1\) this number is \(2\cos(2\pi/n)\).

The definition covers every \(n\) (for \(n = 0\) the exponent \(2\pi i/n\) is read as \(0\), so \(\zeta = 1\)), but results about \(\psi_n\) assume \(n > 2\).

public noncomputable def realCyclotomicPolynomial (n : ℕ) : Polynomial ℤ :=
  minpoly ℤ (Complex.exp (2 * (Real.pi : ℂ) * Complex.I / (n : ℂ)) +
    (Complex.exp (2 * (Real.pi : ℂ) * Complex.I / (n : ℂ)))⁻¹)
Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83-90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex
Used by 4
Used byLehmer's identity for the real cyclotomic polynomial · The real cyclotomic polynomial is the minimal polynomial of \(\zeta + \zeta^{-1}\) · Minimal polynomial of \(2\cos(2\pi k/n)\) for \(k\) coprime to \(n\) · Minimal polynomial of \(2\cos(2\pi k/n)\) for \(1 \le k \le n\) coprime to \(n\)

TheoremMinimal polynomial of \(2\cos(2\pi k/n)\) for \(k\) coprime to \(n\)#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(n > 2\) and \(\gcd(k, n) = 1\). Then the real cyclotomic polynomial \(\psi_n\) equals the minimal polynomial over \(\mathbb{Z}\) of the complex number \(2\cos(2\pi k/n)\).

No bound on \(k\) is needed, since the cosine depends only on \(k\) modulo \(n\).

theorem realCyclotomicPolynomial_eq_minpoly_two_cos
    {n k : ℕ} (hn : 2 < n) (hcop : Nat.Coprime k n) :
    realCyclotomicPolynomial n =
      minpoly ℤ (((2 * Real.cos (2 * (k : ℝ) * Real.pi / (n : ℝ)) : ℝ) : ℂ))
Uses 1 · Used by 1
Statement usesReal cyclotomic polynomial
Used byMinimal polynomial of \(2\cos(2\pi k/n)\) for \(1 \le k \le n\) coprime to \(n\)

TheoremMinimal polynomial of \(2\cos(2\pi k/n)\) for \(1 \le k \le n\) coprime to \(n\)#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(n > 2\), \(1 \le k \le n\) and \(\gcd(k, n) = 1\). Then the real cyclotomic polynomial \(\psi_n\) equals the minimal polynomial over \(\mathbb{Z}\) of the complex number \(2\cos(2\pi k/n)\).

The bounds \(1 \le k \le n\) are not needed: the same holds for every \(k\) coprime to \(n\).

theorem realCyclotomicPolynomial_eq_minpoly_two_cos_of_coprime
    {n k : ℕ} (hn : 2 < n) (hk1 : 1 ≤ k) (hkn : k ≤ n)
    (hcop : Nat.Coprime k n) :
    realCyclotomicPolynomial n =
      minpoly ℤ (((2 * Real.cos (2 * (k : ℝ) * Real.pi / (n : ℝ)) : ℝ) : ℂ))
Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83-90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex
Uses 2
Statement usesReal cyclotomic polynomial
Proof usesMinimal polynomial of \(2\cos(2\pi k/n)\) for \(k\) coprime to \(n\)

TheoremReal cyclotomic polynomial has degree half the totient#●ready to state

For 2 < n, n.totient is even and the natDegree of the real cyclotomic polynomial realCyclotomicPolynomial n equals n.totient / 2. The Even conjunct makes the source's exact half machine-visible under natural-number division.

Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83–90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex

TheoremLehmer's identity for the real cyclotomic polynomial#✓fully proved

Let \(n > 2\) be a natural number, let \(\psi_n\) be the real cyclotomic polynomial, let \(\Phi_n \in \mathbb{Z}[X]\) be the \(n\)-th cyclotomic polynomial, and let \(\varphi\) be Euler's totient function. Then in the ring \(\mathbb{Z}[x, x^{-1}]\) of Laurent polynomials over \(\mathbb{Z}\), \(x^{\varphi(n)/2} \, \psi_n(x + x^{-1}) = \Phi_n(x)\), that is, \(\psi_n(x + x^{-1}) = x^{-\varphi(n)/2} \, \Phi_n(x)\).

theorem lehmer_cyclotomic_identity (n : ℕ) (hn : 2 < n) :
    LaurentPolynomial.T (↑(n.totient / 2)) *
      Polynomial.aeval (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1))
        (realCyclotomicPolynomial n) =
      Polynomial.toLaurent (Polynomial.cyclotomic n ℤ)
Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83-90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex
Uses 1
Statement usesReal cyclotomic polynomial

TheoremThe real cyclotomic polynomial is the minimal polynomial of \(\zeta + \zeta^{-1}\)#✓fully proved

Let \(K\) be a field of characteristic zero, let \(n > 2\) be a natural number, and let \(\zeta \in K\) be a primitive \(n\)-th root of unity. Then the real cyclotomic polynomial \(\psi_n\) equals the minimal polynomial of \(\zeta + \zeta^{-1}\) over \(\mathbb{Z}\).

theorem realCyclotomicPolynomial_eq_minpoly_trace {K : Type*} [Field K]
    [CharZero K] {n : ℕ} (hn : 2 < n) {zeta : K}
    (hprim : IsPrimitiveRoot zeta n) :
    realCyclotomicPolynomial n = minpoly ℤ (zeta + zeta⁻¹)
Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π", Journal of Integer Sequences 19 (2016), source lines 83–90: https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex
Uses 1
Statement usesReal cyclotomic polynomial

TheoremLehmer's theorem on the degree of 2cos(2πk/n)#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(n > 2\) and \(\gcd(k, n) = 1\). Then the \(\mathbb{Q}\)-subalgebra of \(\mathbb{R}\) generated by the real number \(2\cos(2\pi k/n)\) has dimension \(\varphi(n)/2\) as a vector space over \(\mathbb{Q}\), where \(\varphi\) is Euler's totient function.

Since \(n > 2\), \(\varphi(n)\) is even, so \(\varphi(n)/2\) is an integer. Since this dimension is finite and positive, \(2\cos(2\pi k/n)\) is algebraic over \(\mathbb{Q}\) of degree \(\varphi(n)/2\).

theorem finrank_adjoin_two_cos
    (n k : ℕ) (hn : 2 < n) (hk : Nat.Coprime k n) :
    Module.finrank ℚ ↥(Algebra.adjoin ℚ
      ({2 * Real.cos (2 * Real.pi * (k : ℝ) / (n : ℝ))} : Set ℝ)) =
    Nat.totient n / 2
Sources
  • Pinthira Tangsupphathawat and Vichian Laohakosol, "Minimal Polynomials of Algebraic Cosine Values at Rational Multiples of π," Journal of Integer Sequences 19 (2016), Article 16.2.8, Lehmer's theorem recalled in the Introduction, lines 83–90, https://cs.uwaterloo.ca/journals/JIS/VOL19/Laohakosol/lao2.tex
6 fully proved2 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.