mathlib3

db760640 - feat(*): facts about degrees/multiplicites of derivatives (#12856)

feat(*): facts about degrees/multiplicites of derivatives (#12856) For `t` an `n`th repeated root of `p`, we prove that it is an `n-1`th repeated root of `p'` (and tidy the section around this). We also sharpen the theorem stating that `deg p' < deg p`. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>