Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.eval_one_cyclotomic_not_prime_pow

Modification history

2022-06-20 04:10
src/ring_theory/polynomial/cyclotomic/eval.lean
refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463) …
Modified polynomial.eval_one_cyclotomic_not_prime_powView on Github →
2021-12-13 09:36
src/ring_theory/polynomial/cyclotomic/eval.lean
feat(ring_theory/polynomial/cyclotomic/*): ɸₙ(1) = 1 (#10483) …
Added polynomial.eval_one_cyclotomic_not_prime_powView on Github →