Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 10:12 db760640

View on Github →

feat(*): facts about degrees/multiplicites of derivatives (#12856) For t an nth repeated root of p, we prove that it is an n-1th repeated root of p' (and tidy the section around this). We also sharpen the theorem stating that deg p' < deg p.

Estimated changes