Theorems · Theorem · complex analysis
Polynomial.leadingCoeff_le_mahlerMeasure
∀ (p : Polynomial ℂ), ‖p.leadingCoeff‖ ≤ p.mahlerMeasure
- Cited by
- 5 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.
Cites11
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
- mul_oneproof · cited by 3,885
- norm_nonnegproof · cited by 725
- Polynomial.leadingCoeffstatement and proof · cited by 498
- mul_le_mul_of_nonneg_leftproof · cited by 361
- Polynomial.mahlerMeasurestatement and proof · cited by 45
- Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_rootsproof · cited by 4
- Polynomial.one_le_prod_max_one_norm_rootsproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- Polynomial.norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_oneproof · cited by 1
- Polynomial.leadingCoeff_le_mapMahlerMeasureproof · cited by 1
- Polynomial.one_le_mahlerMeasure_of_ne_zeroproof · cited by 0
- Polynomial.one_le_mahlerMeasure_of_one_le_norm_leadingCoeffproof · cited by 0
- Polynomial.leading_coeff_le_mahlerMeasureproof · cited by 0