English
For any nonzero x in K, the product over all finite places w x equals the inverse of the absolute value of the global norm to ℚ, i.e., the product of all local contributions in the finite places recovers the reciprocal of the absolute norm to ℚ.
Русский
Для любого не нулевого x в поле K произведение по всем конечным местам w x равно обратному модулю глобальной нормы к числу ℚ, то есть сумма локальных вкладов в конечных местах восстанавливает обратное абсолютное значение нормa_{ℚ}(x).
LaTeX
$$$\prod_{w \text{ finite place}} w x = |\mathrm{N}_{\mathbb{Q}}^{K}(x)|^{-1}$$$
Lean4
/-- For any non-zero `x` in `K`, the product of `w x`, where `w` runs over `FinitePlace K`, is
equal to the inverse of the absolute value of `Algebra.norm ℚ x`. -/
theorem prod_eq_inv_abs_norm {x : K} (h_x_nezero : x ≠ 0) : ∏ᶠ w : FinitePlace K, w x = |(Algebra.norm ℚ) x|⁻¹ := by
--reduce to 𝓞 K
rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩
apply nonZeroDivisors.ne_zero at hb
have ha : a ≠ 0 := by
rintro rfl
simp at h_x_nezero
simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs,
finprod_div_distrib (mulSupport_finite_int ha) (mulSupport_finite_int hb), prod_eq_inv_abs_norm_int ha,
prod_eq_inv_abs_norm_int hb]
rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]
congr
have hb₀ : ((Algebra.norm ℤ) b : ℝ) ≠ 0 := by simp [hb]
refine (eq_div_of_mul_eq hb₀ ?_).symm
norm_cast
rw [coe_norm_int a, coe_norm_int b, ← MonoidHom.map_mul, div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]
