Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 08:37 dc1484e4

View on Github →

feat(ring_theory/polynomial/cyclotomic): add lemmas about evaluation of cyclotomic polynomials at one (#9910)

Estimated changes

Modified src/ring_theory/polynomial/cyclotomic.lean

added theorem polynomial.eval_one_cyclotomic_prime

added theorem polynomial.eval_one_cyclotomic_prime_pow

added theorem polynomial.eval₂_one_cyclotomic_prime

added theorem polynomial.eval₂_one_cyclotomic_prime_pow