Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.eval₂_one_cyclotomic_prime_pow

Modification history

2021-12-11 21:21

src/ring_theory/polynomial/cyclotomic/basic.lean

feat(ring_theory/polynomial/cyclotomic/eval): `cyclotomic_pos` (#10482)

Modified polynomial.eval₂_one_cyclotomic_prime_pow View on Github →

2021-10-25 08:37

src/ring_theory/polynomial/cyclotomic.lean

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

Added polynomial.eval₂_one_cyclotomic_prime_pow View on Github →