Theorems · Theorem · number theory
Polynomial.one_le_mahlerMeasure_of_ne_zero
∀ {p : Polynomial ℤ}, p ≠ 0 → 1 ≤ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure- Defined in
- Mathlib.NumberTheory.MahlerMeasure
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 299 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
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.normproof · cited by 5,413
- Nat.cast_oneproof · cited by 2,501
- absproof · cited by 1,814
- le_transproof · cited by 985
- Polynomial.mapstatement and proof · cited by 806
- Polynomial.leadingCoeffproof · cited by 498
- Int.cast_oneproof · cited by 371
- Int.castRingHomstatement and proof · cited by 254
- eq_intCastproof · cited by 127
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.