mathlib

ae93ce85 - 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