Commit 2026-01-26 08:43 291723f1

View on Github →

feat(Algebra/Polynomial/Splits): add Splits.image_rootSet_of_monic (#34046) This PR adds a new lemma Splits.image_rootSet_of_monic as well as extracting some commonly used variables to the top of the section. I also took the liberty of removing the IsSimpleRing R assumption from Splits.aeval_eq_prod_aroots_of_monic.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

modified theorem Polynomial.Splits.adjoin_rootSet_eq_range

modified theorem Polynomial.Splits.aeval_eq_prod_aroots

modified theorem Polynomial.Splits.aeval_eq_prod_aroots_of_monic

modified theorem Polynomial.Splits.image_rootSet

added theorem Polynomial.Splits.image_rootSet_of_map_ne_zero

deleted theorem Polynomial.Splits.map_roots

added theorem Polynomial.Splits.roots_map

added theorem Polynomial.Splits.roots_map_of_injective

added theorem Polynomial.Splits.roots_map_of_ne_zero

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean