Commit 2024-10-30 08:37 153aff57

View on Github →

feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (x + algebraMap K L a) splits (#17093) We show that minpoly K x splits implies minpoly K (x + algebraMap K L a) splits.

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.dvd_comp_X_add_C_iff

added theorem Polynomial.dvd_comp_X_sub_C_iff

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.Splits.comp_X_add_C

added theorem Polynomial.Splits.comp_X_sub_C

Modified Mathlib/FieldTheory/Minpoly/Field.lean

modified theorem minpoly.sub_algebraMap

Modified Mathlib/RingTheory/Adjoin/Field.lean

added theorem minpoly_add_algebraMap_splits

added theorem minpoly_algebraMap_add_splits

added theorem minpoly_sub_algebraMap_splits