# 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.

theorem Counterexample.properDivisors_105 :
= {1, 3, 5, 7, 15, 21, 35}
theorem Counterexample.cyclotomic_3 :
= 1 + Polynomial.X + Polynomial.X ^ 2
theorem Counterexample.cyclotomic_5 :
= 1 + Polynomial.X + Polynomial.X ^ 2 + Polynomial.X ^ 3 + Polynomial.X ^ 4
theorem Counterexample.cyclotomic_7 :
= 1 + Polynomial.X + Polynomial.X ^ 2 + Polynomial.X ^ 3 + Polynomial.X ^ 4 + Polynomial.X ^ 5 + Polynomial.X ^ 6
theorem Counterexample.cyclotomic_15 :
= 1 - Polynomial.X + Polynomial.X ^ 3 - Polynomial.X ^ 4 + Polynomial.X ^ 5 - Polynomial.X ^ 7 + Polynomial.X ^ 8
theorem Counterexample.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 :
= 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 :
= 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