Commit 2023-12-13 19:05 8a221878

feat(Data/Polynomial/RingDivision): improvements to Polynomial.rootMultiplicity (#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.