Theorem Polynomial.cyclotomic.eval_apply_ofReal

Modification history

2025-01-09 23:52
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
chore: clean up some `erw` in cyclotomic polynomials (#20597)
Added Polynomial.cyclotomic.eval_apply_ofRealView on Github →