Theorem Polynomial.comp_neg_X_leadingCoeff_eq

Modification history

2024-12-02 07:36
Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
feat(Polynomial): new lemmas and noncommutative generalizations (#19665) …
Modified Polynomial.comp_neg_X_leadingCoeff_eqView on Github →
2024-10-22 13:55
Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
chore(Algebra/Polynomial/RingDivision): move lemmas earlier (#18050) …
Modified Polynomial.comp_neg_X_leadingCoeff_eqView on Github →
2024-10-07 20:10
Mathlib/Algebra/Polynomial/RingDivision.lean
feat(FieldTheory/Minpoly): add theorem for minpoly of -x (#17367) …
Added Polynomial.comp_neg_X_leadingCoeff_eqView on Github →