fact: Fixpoint list_root_multiplicity α {r : ring α} {K : field r} (acf : algeb_closed_field K) c la d := match d with | O => O | S d₁ => if fld_zerop (lap_mod_deg_1 la c) then S (list_root_multiplicity acf c (lap_div_deg_1 la c) d₁) else O end.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn