Commit 2024-12-23 14:21 9acfd2fc

feat: the product formula for number fields (#20132) In this file we prove the Product Formula for number fields: for any non-zero element x of a number field K, we have ∏|x|ᵥ=1 where the product runs over the equivalence classes of absoulte values of K and the |⬝|ᵥ are suitably normalized.

Main Results

• NumberField.FinitePlace.prod_eq_inv_abs_norm: for any non-zero element x of a number field K, the product ∏|x|ᵥ of the absolute values of x associated to the finite places of K is equal to the inverse of the norm of x.
• NumberField.prod_abs_eq_one: for any non-zero element x of a number field K, we have ∏|x|ᵥ=1 where the product runs over the equivalence classes of absoulte values of K.