∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.mulHeight x =
    if x = 0 then 1
    else
      (Multiset.map (fun v => ⨆ i, v (x i)) Height.AdmissibleAbsValues.archAbsVal).prod *
        ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ i, ↑v (x i)