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.

@[protected, instance]
@[protected, instance]
theorem counterexample.proper_divisors_105  :
105.proper_divisors = {1, 3, 5, 7, 15, 21, 35}