Commit 2024-10-07 20:10 312b6226

View on Github →

feat(FieldTheory/Minpoly): add theorem for minpoly of -x (#17367) Add theorem minpoly A (- x) = (-1) ^ (natDegree (minpoly A x)) * (minpoly A x).comp (- X)

Estimated changes

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added theorem Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X

added theorem Polynomial.comp_neg_X_leadingCoeff_eq

Modified Mathlib/FieldTheory/Minpoly/Field.lean

added theorem minpoly.neg

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

added theorem IsIntegral.neg_iff

added theorem IsIntegral.of_neg

added theorem RingHom.IsIntegralElem.neg_iff

added theorem RingHom.IsIntegralElem.of_neg