∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] {x : ι → K},
  x ≠ 0 → ∀ {y : ι' → K}, y ≠ 0 → (Height.logHeight fun a => x a.1 * y a.2) = Height.logHeight x + Height.logHeight y