Commit 2024-11-19 08:56 a5783c91

View on Github →

feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits (#17369) Add minpoly K x splits implies minpoly K (- x) splits and minpoly K (algebraMap K L a - x) splits. This is after #17093 .

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added def Polynomial.algEquivAevalNegX

modified def Polynomial.algEquivAevalXAddC

modified theorem Polynomial.algEquivAevalXAddC_eq_iff

modified theorem Polynomial.algEquivAevalXAddC_symm

added def Polynomial.algEquivCMulXAddC

added theorem Polynomial.algEquivCMulXAddC_symm_eq

added theorem Polynomial.comp_neg_X_comp_neg_X

added theorem Polynomial.dvd_comp_C_mul_X_add_C_iff

added theorem Polynomial.dvd_comp_neg_X_iff

Modified Mathlib/Algebra/Polynomial/Splits.lean

modified theorem Polynomial.Splits.comp_X_add_C

modified theorem Polynomial.Splits.comp_X_sub_C

added theorem Polynomial.Splits.comp_neg_X

added theorem Polynomial.Splits.comp_of_degree_le_one

added theorem Polynomial.Splits.comp_of_map_degree_le_one

added theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one

Modified Mathlib/RingTheory/Adjoin/Field.lean

added theorem minpoly_algebraMap_sub_splits

added theorem minpoly_neg_splits