Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 00:55 d6056eee

View on Github →

feat(field_theory/splitting_field): add eval_root_derivative_of_split (#10224) From flt-regular.

Estimated changes

Modified src/data/polynomial/derivative.lean

added theorem polynomial.derivative_prod

added theorem polynomial.eval_multiset_prod_X_sub_C_derivative

Modified src/field_theory/splitting_field.lean

added theorem polynomial.aeval_root_derivative_of_splits