Theorems · Theorem · complex analysis
Polynomial.mahlerMeasure_def_of_ne_zero
∀ {p : Polynomial ℂ},
p ≠ 0 →
p.mahlerMeasure =
Real.exp ((2 * Real.pi)⁻¹ * ∫ (x : ℝ) in 0..2 * Real.pi, Real.log ‖Polynomial.eval (circleMap 0 1 x) p‖)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 254 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Real.pistatement and proof · cited by 1,774
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- Real.logstatement and proof · cited by 939
- Real.expstatement and proof · cited by 871
- Polynomial.evalstatement and proof · cited by 796
- intervalIntegralstatement and proof · cited by 546
- mul_inv_revproof · cited by 270
- circleMapstatement and proof · cited by 117
Cited by3
Results whose statement or proof uses this declaration.
- Polynomial.mahlerMeasure_nonnegproof · cited by 3
- Polynomial.mahlerMeasure_le_sum_norm_coeffproof · cited by 1
- Polynomial.mahlerMeasure_eq_zero_iffproof · cited by 0