Theorems · Theorem · complex analysis
Polynomial.IsRoot.norm_lt_cauchyBound
∀ {K : Type u_1} [inst : NormedDivisionRing K] {p : Polynomial K}, p ≠ 0 → ∀ {a : K}, p.IsRoot a → ‖a‖₊ < p.cauchyBoundcauchyBound is a bound on the norm of polynomial roots.
- Defined in
- Mathlib.Analysis.Polynomial.CauchyBound
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedDivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites64
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Polynomialstatement and proof · cited by 5,681
- Finset.sumproof · cited by 5,195
- NNRealstatement and proof · cited by 4,310
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- Finset.sum_congrproof · cited by 2,323
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- MulZeroClass.zero_mulproof · cited by 1,625
- Finset.rangeproof · cited by 1,341
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.