Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Data/Polynomial/RingDivision): improvements to `Polynomial.rootM…
…ultiplicity` (#8563) Main changes: - add `Monic.mem_nonZeroDivisors` and `mem_nonZeroDivisors_of_leadingCoeff` which states that a monic polynomial (resp. a polynomial whose leading coefficient is not zero divisor) is not a zero divisor. - add `rootMultiplicity_mul_X_sub_C_pow` which states that `* (X - a) ^ n` adds the root multiplicity at `a` by `n`. - change the conditions in `rootMultiplicity_X_sub_C_self`, `rootMultiplicity_X_sub_C` and `rootMultiplicity_X_sub_C_pow` from `IsDomain` to `Nontrivial`. - add `rootMultiplicity_eq_natTrailingDegree` which relates `rootMultiplicity` and `natTrailingDegree`, and `eval_divByMonic_eq_trailingCoeff_comp`. - add `le_rootMultiplicity_mul` which is similar to `le_trailingDegree_mul`. - add `rootMultiplicity_mul'` which slightly generalizes `rootMultiplicity_mul` In `Data/Polynomial/FieldDivision`: - add `rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero` which slightly generalizes `rootMultiplicity_sub_one_le_derivative_rootMultiplicity`. - add `derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors` which slightly generalizes `derivative_rootMultiplicity_of_root`. - add several theorems relating roots of iterate derivative to `rootMultiplicity` In addition: - move `eq_of_monic_of_associated` from RingDivision to Monic and generalize. - add `dvd_cancel` lemmas to NonZeroDivisors. - add `algEquivOfCompEqX`: two polynomials that compose to X both ways induces an isomorphism of the polynomial algebra. - add divisibility lemmas to Polynomial/Derivative. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
- Loading branch information
1 parent
c4988d1
commit 8a22187
Showing
10 changed files
with
326 additions
and
76 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.