prod_abs_eq_one — Mathlib

English

For any nonzero x in the number field K, the product of the infinite place contributions and the finite place contributions equals 1.

Русский

Для любого не нулевого x в числовом поле K произведение вкладов бесконечных мест и конечных мест даёт 1.

LaTeX

$$$\left(\prod_{w \in \mathrm{InfinitePlace}(K)} w x^{\mathrm{mult}(w)}\right) \cdot \left(\prod_{w \text{ finite place}} w x\right) = 1$$$

Lean4

/-- The Product Formula for the Number Field `K`. -/
theorem prod_abs_eq_one {x : K} (h_x_nezero : x ≠ 0) :
    (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ w : FinitePlace K, w x = 1 := by
  simp [prod_eq_inv_abs_norm, InfinitePlace.prod_eq_abs_norm, h_x_nezero]

Похожие утверждения