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_15 :
Eq (Nat.properDivisors 15) (Insert.insert 1 (Insert.insert 3 (Singleton.singleton 5)))
theorem
Counterexample.properDivisors_21 :
Eq (Nat.properDivisors 21) (Insert.insert 1 (Insert.insert 3 (Singleton.singleton 7)))
theorem
Counterexample.properDivisors_35 :
Eq (Nat.properDivisors 35) (Insert.insert 1 (Insert.insert 5 (Singleton.singleton 7)))
theorem
Counterexample.properDivisors_105 :
Eq (Nat.properDivisors 105)
(Insert.insert 1
(Insert.insert 3
(Insert.insert 5 (Insert.insert 7 (Insert.insert 15 (Insert.insert 21 (Singleton.singleton 35)))))))
theorem
Counterexample.cyclotomic_3 :
Eq (Polynomial.cyclotomic 3 Int) (HAdd.hAdd (HAdd.hAdd 1 Polynomial.X) (HPow.hPow Polynomial.X 2))
theorem
Counterexample.cyclotomic_5 :
Eq (Polynomial.cyclotomic 5 Int)
(HAdd.hAdd (HAdd.hAdd (HAdd.hAdd (HAdd.hAdd 1 Polynomial.X) (HPow.hPow Polynomial.X 2)) (HPow.hPow Polynomial.X 3))
(HPow.hPow Polynomial.X 4))
theorem
Counterexample.cyclotomic_7 :
Eq (Polynomial.cyclotomic 7 Int)
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd (HAdd.hAdd (HAdd.hAdd 1 Polynomial.X) (HPow.hPow Polynomial.X 2)) (HPow.hPow Polynomial.X 3))
(HPow.hPow Polynomial.X 4))
(HPow.hPow Polynomial.X 5))
(HPow.hPow Polynomial.X 6))
theorem
Counterexample.cyclotomic_15 :
Eq (Polynomial.cyclotomic 15 Int)
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub (HAdd.hAdd (HSub.hSub 1 Polynomial.X) (HPow.hPow Polynomial.X 3)) (HPow.hPow Polynomial.X 4))
(HPow.hPow Polynomial.X 5))
(HPow.hPow Polynomial.X 7))
(HPow.hPow Polynomial.X 8))
theorem
Counterexample.cyclotomic_21 :
Eq (Polynomial.cyclotomic 21 Int)
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub (HAdd.hAdd (HSub.hSub 1 Polynomial.X) (HPow.hPow Polynomial.X 3)) (HPow.hPow Polynomial.X 4))
(HPow.hPow Polynomial.X 6))
(HPow.hPow Polynomial.X 8))
(HPow.hPow Polynomial.X 9))
(HPow.hPow Polynomial.X 11))
(HPow.hPow Polynomial.X 12))
theorem
Counterexample.cyclotomic_35 :
Eq (Polynomial.cyclotomic 35 Int)
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub
(HAdd.hAdd
(HSub.hSub (HAdd.hAdd (HSub.hSub 1 Polynomial.X) (HPow.hPow Polynomial.X 5))
(HPow.hPow Polynomial.X 6))
(HPow.hPow Polynomial.X 7))
(HPow.hPow Polynomial.X 8))
(HPow.hPow Polynomial.X 10))
(HPow.hPow Polynomial.X 11))
(HPow.hPow Polynomial.X 12))
(HPow.hPow Polynomial.X 13))
(HPow.hPow Polynomial.X 14))
(HPow.hPow Polynomial.X 16))
(HPow.hPow Polynomial.X 17))
(HPow.hPow Polynomial.X 18))
(HPow.hPow Polynomial.X 19))
(HPow.hPow Polynomial.X 23))
(HPow.hPow Polynomial.X 24))
theorem
Counterexample.cyclotomic_105 :
Eq (Polynomial.cyclotomic 105 Int)
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HAdd.hAdd
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HSub.hSub
(HAdd.hAdd (HAdd.hAdd 1 Polynomial.X)
(HPow.hPow Polynomial.X 2))
(HPow.hPow Polynomial.X 5))
(HPow.hPow Polynomial.X 6))
(HMul.hMul 2 (HPow.hPow Polynomial.X 7)))
(HPow.hPow Polynomial.X 8))
(HPow.hPow Polynomial.X 9))
(HPow.hPow Polynomial.X 12))
(HPow.hPow Polynomial.X 13))
(HPow.hPow Polynomial.X 14))
(HPow.hPow Polynomial.X 15))
(HPow.hPow Polynomial.X 16))
(HPow.hPow Polynomial.X 17))
(HPow.hPow Polynomial.X 20))
(HPow.hPow Polynomial.X 22))
(HPow.hPow Polynomial.X 24))
(HPow.hPow Polynomial.X 26))
(HPow.hPow Polynomial.X 28))
(HPow.hPow Polynomial.X 31))
(HPow.hPow Polynomial.X 32))
(HPow.hPow Polynomial.X 33))
(HPow.hPow Polynomial.X 34))
(HPow.hPow Polynomial.X 35))
(HPow.hPow Polynomial.X 36))
(HPow.hPow Polynomial.X 39))
(HPow.hPow Polynomial.X 40))
(HMul.hMul 2 (HPow.hPow Polynomial.X 41)))
(HPow.hPow Polynomial.X 42))
(HPow.hPow Polynomial.X 43))
(HPow.hPow Polynomial.X 46))
(HPow.hPow Polynomial.X 47))
(HPow.hPow Polynomial.X 48))
theorem
Counterexample.not_forall_coeff_cyclotomic_neg_one_zero_one :
Not
(∀ (n i : Nat),
Membership.mem (Insert.insert (-1) (Insert.insert 0 (Singleton.singleton 1)))
((Polynomial.cyclotomic n Int).coeff i))