Commit 2024-02-10 09:09 e7a73bf3

View on Github →

feat(PerfectRing): roots of Polynomial.expand (#9311) Inspired by #9271 Prove the main theorem rootMultiplicity_expand and derive corollaries about Polynomial.roots. Refactor rootsExpand(Pow)EquivRoots using the new lemmas.

Estimated changes

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.isRoot_comp

Modified Mathlib/Data/Polynomial/Expand.lean

added theorem Polynomial.expand_eq_comp_X_pow

added theorem Polynomial.rootMultiplicity_expand

added theorem Polynomial.rootMultiplicity_expand_pow

Modified Mathlib/FieldTheory/Perfect.lean

added theorem Polynomial.rootsExpandPowToRoots_apply

added theorem Polynomial.rootsExpandToRoots_apply

added theorem Polynomial.roots_expand

added theorem Polynomial.roots_expand_image_frobenius

added theorem Polynomial.roots_expand_image_frobenius_subset

added theorem Polynomial.roots_expand_image_iterateFrobenius

added theorem Polynomial.roots_expand_map_frobenius

added theorem Polynomial.roots_expand_map_frobenius_le

added theorem Polynomial.roots_expand_pow

added theorem Polynomial.roots_expand_pow_image_iterateFrobenius_subset

added theorem Polynomial.roots_expand_pow_map_iterateFrobenius

added theorem Polynomial.roots_expand_pow_map_iterateFrobenius_le

added theorem iterateFrobeniusEquiv_eq_pow

added theorem iterateFrobeniusEquiv_symm