theorem NumberField.product_formula {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1