Closed Zimmi48 closed 7 years ago
Actually the complete statement is:
puiseux_series_algeb_closed
: ∀ (α : Type) (R : ring α) (K : field R),
algeb_closed_field K
→ ∀ pol : polynomial (puiseux_series α),
degree (ps_zerop K) pol ≥ 1
→ ∃ s : puiseux_series α, (ps_pol_apply pol s = 0)%ps
The statement of the theorem appeared in a section, thus K
was not explicitly defined.
Daniel de Rauglaudre explained to me that R
became K
following notation changes.
I am going to update the PR.
Nice! Thank you.
Thanks! Any reason for K rather than R?