Homogenized cyclotomic polynomials

DefinitionHomogenized cyclotomic value#✓fully proved

For a natural number \(n\) and integers \(a, b\), let \(c_0, \dots, c_{\varphi(n)}\) be the integer coefficients of the \(n\)-th cyclotomic polynomial, whose degree is \(\varphi(n)\), where \(\varphi\) is Euler's totient function. The homogenized cyclotomic value is the integer

\[\Phi_n(a, b) = \sum_{i=0}^{\varphi(n)} c_i \, a^i \, b^{\varphi(n) - i}.\]

When \(b \neq 0\) it equals \(b^{\varphi(n)} \Phi_n(a/b)\), where \(\Phi_n\) is the \(n\)-th cyclotomic polynomial.

public noncomputable def homogenizedCyclotomic (n : ℕ) (a b : ℤ) : ℤ :=
  ∑ i ∈ Finset.range (Nat.totient n + 1),
    (cyclotomic n ℤ).coeff i * a ^ i * b ^ (Nat.totient n - i)

Sources

• Ömer Avcı, Large Zsigmondy Primes, INTEGERS 24 (2024), Article A62, Section 2 (notation Φ_n(a, b), Lemma 3 and the explicit values in the proof of Theorem 1).

Used by 13

Used byHomogenized cyclotomic value in a field · Homogenized cyclotomic value of index one · Homogenized cyclotomic value with second argument one · Homogenized cyclotomic value of index two · Zsigmondy primes divide the homogenized cyclotomic value · A size criterion for a large Zsigmondy prime · Bounds for homogenized cyclotomic values · Homogenized cyclotomic values at \(pn\) · Homogenized cyclotomic values at \(p^\beta k\) · \(p\)-adic valuation of homogenized cyclotomic values at an odd prime · \(2\)-adic valuation of homogenized cyclotomic values · Prime divisors of homogenized cyclotomic values · Factorization of \(a^n - b^n\) into homogenized cyclotomic values

TheoremHomogenized cyclotomic value of index one#✓fully proved

For all integers \(a\) and \(b\), the homogenized cyclotomic value \(\Phi_1(a, b)\) equals \(a - b\).

public theorem homogenizedCyclotomic_one (a b : ℤ) : homogenizedCyclotomic 1 a b = a - b

Sources

• Ömer Avcı, Large Zsigmondy Primes, INTEGERS 24 (2024), Article A62, Lemma 3 (v) (the case n = 1).

Uses 1

Statement usesHomogenized cyclotomic value

TheoremHomogenized cyclotomic value of index two#✓fully proved

For all integers \(a\) and \(b\), the homogenized cyclotomic value \(\Phi_2(a, b)\) equals \(a + b\).

public theorem homogenizedCyclotomic_two (a b : ℤ) : homogenizedCyclotomic 2 a b = a + b

Sources

• Ömer Avcı, Large Zsigmondy Primes, INTEGERS 24 (2024), Article A62, Lemma 3 (v) (the case n = 2).

Uses 1

Statement usesHomogenized cyclotomic value

TheoremHomogenized cyclotomic value with second argument one#✓fully proved

For every natural number \(n\) and every integer \(a\), the homogenized cyclotomic value \(\Phi_n(a, 1)\) equals \(\Phi_n(a)\), the value at \(a\) of the \(n\)-th cyclotomic polynomial with integer coefficients.

public theorem homogenizedCyclotomic_one_right (n : ℕ) (a : ℤ) :
    homogenizedCyclotomic n a 1 = (cyclotomic n ℤ).eval a

Sources

• Ömer Avcı, Large Zsigmondy Primes, INTEGERS 24 (2024), Article A62, Section 2 (notation Φ_n(a, b)).

Uses 1

Statement usesHomogenized cyclotomic value

TheoremHomogenized cyclotomic value in a field#✓fully proved

Let \(K\) be a field, \(n\) a natural number and \(a, b\) integers such that the image of \(b\) in \(K\) is nonzero. Then the image in \(K\) of the homogenized cyclotomic value \(\Phi_n(a, b)\) equals \(b^{\varphi(n)} \Phi_n(a/b)\), where \(\Phi_n\) is the \(n\)-th cyclotomic polynomial over \(K\), \(\varphi\) is Euler's totient function, and \(b\) and \(a/b\) are computed in \(K\).

public theorem homogenizedCyclotomic_cast {K : Type*} [Field K] (n : ℕ) (a b : ℤ)
    (hb : (b : K) ≠ 0) :
    ((homogenizedCyclotomic n a b : ℤ) : K) =
      (b : K) ^ Nat.totient n * (cyclotomic n K).eval ((a : K) / (b : K))

Sources

• Ömer Avcı, Large Zsigmondy Primes, INTEGERS 24 (2024), Article A62, Section 2 (notation Φ_n(a, b)).

Uses 1

Statement usesHomogenized cyclotomic value

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.