mathlib3 documentation

mathlib-counterexamples / cyclotomic_105

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
def counterexample.nat.fact_prime_five  :
fact (nat.prime 5)
source
@[protected, instance]
def counterexample.nat.fact_prime_seven  :
fact (nat.prime 7)
source
theorem counterexample.proper_divisors_15  :
15.proper_divisors = {1, 3, 5}
source
theorem counterexample.proper_divisors_21  :
21.proper_divisors = {1, 3, 7}
source
theorem counterexample.proper_divisors_35  :
35.proper_divisors = {1, 5, 7}
source
theorem counterexample.proper_divisors_105  :
105.proper_divisors = {1, 3, 5, 7, 15, 21, 35}
source
theorem counterexample.cyclotomic_3  :
polynomial.cyclotomic 3 ℤ = 1 + polynomial.X + polynomial.X ^ 2
source
theorem counterexample.cyclotomic_5  :
polynomial.cyclotomic 5 ℤ = 1 + polynomial.X + polynomial.X ^ 2 + polynomial.X ^ 3 + polynomial.X ^ 4
source
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
source
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
source
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
source
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
source
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
source
theorem counterexample.coeff_cyclotomic_105  :
(polynomial.cyclotomic 105 ℤ).coeff 7 = -2
source
theorem counterexample.not_forall_coeff_cyclotomic_neg_one_zero_one  :
¬∀ (n i : ℕ), (polynomial.cyclotomic n ℤ).coeff i ∈ {-1, 0, 1}