Not all coefficients of cyclotomic polynomials are -1, 0, or 1

We show that not all coefficients of cyclotomic polynomials are equal to 0, -1 or 1, in the theorem not_forall_coeff_cyclotomic_neg_one_zero_one. We prove this with the counterexample coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2.

instance Counterexample.Nat.fact_prime_five : Fact (Nat.Prime 5)

Equations

• Counterexample.Nat.fact_prime_five = ⋯

instance Counterexample.Nat.fact_prime_seven : Fact (Nat.Prime 7)

Equations

• Counterexample.Nat.fact_prime_seven = ⋯

theorem Counterexample.properDivisors_15 : Nat.properDivisors 15 = {1, 3, 5}

theorem Counterexample.properDivisors_21 : Nat.properDivisors 21 = {1, 3, 7}

theorem Counterexample.properDivisors_35 : Nat.properDivisors 35 = {1, 5, 7}

theorem Counterexample.properDivisors_105 : Nat.properDivisors 105 = {1, 3, 5, 7, 15, 21, 35}

theorem Counterexample.cyclotomic_3 : Polynomial.cyclotomic 3 ℤ = 1 + Polynomial.X + Polynomial.X ^ 2

theorem Counterexample.cyclotomic_5 : Polynomial.cyclotomic 5 ℤ = 1 + Polynomial.X + Polynomial.X ^ 2 + Polynomial.X ^ 3 + Polynomial.X ^ 4

theorem Counterexample.cyclotomic_7 : Polynomial.cyclotomic 7 ℤ = 1 + Polynomial.X + Polynomial.X ^ 2 + Polynomial.X ^ 3 + Polynomial.X ^ 4 + Polynomial.X ^ 5 + Polynomial.X ^ 6

theorem Counterexample.cyclotomic_15 : Polynomial.cyclotomic 15 ℤ = 1 - Polynomial.X + Polynomial.X ^ 3 - Polynomial.X ^ 4 + Polynomial.X ^ 5 - Polynomial.X ^ 7 + Polynomial.X ^ 8

theorem Counterexample.cyclotomic_21 : Polynomial.cyclotomic 21 ℤ = 1 - Polynomial.X + Polynomial.X ^ 3 - Polynomial.X ^ 4 + Polynomial.X ^ 6 - Polynomial.X ^ 8 + Polynomial.X ^ 9 - Polynomial.X ^ 11 + Polynomial.X ^ 12

theorem Counterexample.cyclotomic_35 : Polynomial.cyclotomic 35 ℤ = 1 - Polynomial.X + Polynomial.X ^ 5 - Polynomial.X ^ 6 + Polynomial.X ^ 7 - Polynomial.X ^ 8 + Polynomial.X ^ 10 - Polynomial.X ^ 11 + Polynomial.X ^ 12 - Polynomial.X ^ 13 + Polynomial.X ^ 14 - Polynomial.X ^ 16 + Polynomial.X ^ 17 - Polynomial.X ^ 18 + Polynomial.X ^ 19 - Polynomial.X ^ 23 + Polynomial.X ^ 24

theorem Counterexample.cyclotomic_105 : Polynomial.cyclotomic 105 ℤ = 1 + Polynomial.X + Polynomial.X ^ 2 - Polynomial.X ^ 5 - Polynomial.X ^ 6 - 2 * Polynomial.X ^ 7 - Polynomial.X ^ 8 - Polynomial.X ^ 9 + Polynomial.X ^ 12 + Polynomial.X ^ 13 + Polynomial.X ^ 14 + Polynomial.X ^ 15 + Polynomial.X ^ 16 + Polynomial.X ^ 17 - Polynomial.X ^ 20 - Polynomial.X ^ 22 - Polynomial.X ^ 24 - Polynomial.X ^ 26 - Polynomial.X ^ 28 + Polynomial.X ^ 31 + Polynomial.X ^ 32 + Polynomial.X ^ 33 + Polynomial.X ^ 34 + Polynomial.X ^ 35 + Polynomial.X ^ 36 - Polynomial.X ^ 39 - Polynomial.X ^ 40 - 2 * Polynomial.X ^ 41 - Polynomial.X ^ 42 - Polynomial.X ^ 43 + Polynomial.X ^ 46 + Polynomial.X ^ 47 + Polynomial.X ^ 48

theorem Counterexample.coeff_cyclotomic_105 : (Polynomial.cyclotomic 105 ℤ).coeff 7 = -2

theorem Counterexample.not_forall_coeff_cyclotomic_neg_one_zero_one : ¬∀ (n i : ℕ), (Polynomial.cyclotomic n ℤ).coeff i ∈ {-1, 0, 1}