Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-24 11:01 8ff2783f

View on Github →

feat(counterexamples/cyclotomic_105): add coeff_cyclotomic_105 (#7648) We show that coeff (cyclotomic 105 ℤ) 7 = -2, proving that not all coefficients of cyclotomic polynomials are 0, -1 or 1.

Estimated changes

added theorem coeff_cyclotomic_105
added theorem cyclotomic_105
added theorem cyclotomic_15
added theorem cyclotomic_21
added theorem cyclotomic_35
added theorem cyclotomic_3
added theorem cyclotomic_5
added theorem cyclotomic_7
added theorem prime_3
added theorem prime_5
added theorem prime_7
added theorem proper_divisors_105
added theorem proper_divisors_15
added theorem proper_divisors_21
added theorem proper_divisors_35