feat(topology/algebra/polynomial): add coeff_le_of_roots_le (#15275)
feat(topology/algebra/polynomial): add coeff_le_of_roots_le (#15275)

This is the proof that, if the roots of a polynomial are bounded, then its coefficients are bounded. More precisely, it is the following statement: 
```lean
lemma coeff_le_of_roots_le [field F] [normed_field K] {p : F[X]} {f : F  →+* K} {B : ℝ} (i : ℕ) 
(h1 : p.monic) (h2 : splits f p) (h3 : ∀ z ∈ (map f p).roots, ∥z∥ ≤ B) :
  ∥ (map f p).coeff i ∥ ≤ B^(p.nat_degree - i) * p.nat_degree.choose i 
```

From flt-regular
 




leanprover-community/mathlib,leanprover-community/mathlib