Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-09 23:52
b85c65bb
View on Github →
chore: clean up some
erw
in cyclotomic polynomials (
#20597
)
Estimated changes
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
added
theorem
Polynomial.cyclotomic.eval_apply_ofReal
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean