Theorems · Theorem · complex analysis
Polynomial.norm_coeff_le_choose_mul_mahlerMeasure
∀ (n : ℕ) (p : Polynomial ℂ), ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites79
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Polynomialstatement and proof · cited by 5,681
- Complexstatement and proof · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- Finset.sumproof · cited by 5,195
- one_mulproof · cited by 2,841
- Multisetproof · cited by 2,627
- Nat.cast_oneproof · cited by 2,501
- Finset.prodproof · cited by 2,356
- Finset.sum_congrproof · cited by 2,323
- MulZeroClass.mul_zeroproof · cited by 2,091
- mul_assocproof · cited by 1,667
Cited by3
Results whose statement or proof uses this declaration.
- Polynomial.supNorm_le_choose_natDegree_div_two_mul_mahlerMeasureproof · cited by 0
- Polynomial.norm_coeff_le_choose_mul_mapMahlerMeasureproof · cited by 0