Product formula for the rationals

Stream: mathlib4

[Fabrizio Barroero]

As a warm-up for the general case over number fields, I proved the product formula over $\mathbb{Q}$. This is the theorem

theorem product_formula {x : ℚ} (h_x_nezero : x ≠ 0) : |x| * ∏ᶠ p : Nat.Primes, padicNorm p x = 1

I have reduced the statement to the naturals and then to

theorem product_formula_N_range {x : ℕ} (h_x_nezero : x ≠ 0) : |(x : ℚ)| *
    ∏ p ∈ Finset.filter Nat.Prime (Finset.range (x + 1)), padicNorm p x = 1

in order to use docs#Nat.prod_pow_prime_padicValNat.

Do you guys think it can go to Mathlib? If so, where? In Mathlib.NumberTheory.Padics.PadicNorm?

[Michael Stoll]

This should definitely be in Mathlib! You could try #find_home! product_formula_N_range to see possible files where it could go.

[Filippo A. E. Nuccio]

This must certainly be in Mathlib, I agree!

[Filippo A. E. Nuccio]

I think it is a general result about number fields, so nor really related to padic numbers.

[Filippo A. E. Nuccio]

I think that a dedicated file ProductFormula inside Mathlib/NumberTheory/NumberFields would be good. It will eventually contain the product formula for more general number fields.

[David Ang]

Thanks! I've been waiting for this for my heights PR.

[Kevin Buzzard]

Right now our definition of adeles of a number field $F$ is looking like it's going to be restricted product of completions. But another definition could be $\mathbb{A}_{\mathbb{Q}}\otimes_{\mathbb{Q}}F$ (these are canonically isomorphic but this is a theorem). If we use this latter definition can we somehow get product formula for general number fields from the statement for $\mathbb{Q}$? I would have thought that the proof that the two definitions of $\mathbb{A}_F$ coincided was almost all local and in particular won't use the product formula

[Kevin Buzzard]

This norm is defined purely intrinsically, the adeles are a locally compact space so possess a Haar measure, and the norm of an idele x is the factor that the haar measure is scaled by when you multiply by x.

[Fabrizio Barroero]

Thanks everyone for the feedback.
#find_home! product_formula gives Mathlib.NumberTheory.Padics.PadicNumbers, Mathlib.NumberTheory.Ostrowski while
#find_home! product_formula_N_range gives Mathlib.
In both cases I think #find_home! did not do a good job.
I agree that the product formula for number fields should have its own file, but I thought this one could go in the PadicNorm file as it is pretty elementary.
I will prepare a PR in the next few days.