Subadditivity of the logarithmic height under multiplication
Provedbaker_height_mul_leheightsnumber-theory
The logarithmic Weil height is subadditive under multiplication: for elements x, y of a field with admissible absolute values, h(xy) is at most h(x) + h(y). This is the basic height calculus used in every Baker-type Diophantine application.
Preamble
import Mathlib.NumberTheory.Height.Basic
Formal statement
theorem baker_height_mul_le {K : Type*} [Field K] [Height.AdmissibleAbsValues K] (x y : K) : Height.logHeight₁ (x * y) ≤ Height.logHeight₁ x + Height.logHeight₁ y := by sorrySource