fact: Definition root_multiplicity α {r : ring α} {K : field r} (acf : algeb_closed_field K) c f := list_root_multiplicity acf c (al f) (List.length (al f)).
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn