Theorem Polynomial.sub_one_pow_totient_le_cyclotomic_eval

Modification history

2023-06-16 17:18
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
feat: port RingTheory.Polynomial.Cyclotomic.Eval (#5144)
Added Polynomial.sub_one_pow_totient_le_cyclotomic_evalView on Github →