Preferred spelling of p-adic valuation?

Stream: Is there code for X?

[Michael Stoll]

I'm working on dealing with the TODO in number_theory.sum_two_squares. I'm basically done, but it is not clear to me what is the best way to state the condition "the exponent of p in the prime factorization of n is even". More precisely, how to express "the exponent of p in the prime factorization of n". There are (at least) three possibilities (this is lean3+mathlib):

1. multiplicity p n
2. padic_val_nat p n
3. n.factorization p

The first takes values in part_enat, which makes it a bit fiddly to work with -- here is a challenge: prove

example {p n : ℕ} (hp : p.prime) (hn : n ≠ 0) : ¬ even (2 • multiplicity p n + 1) := sorry

The second is a wrapper around multiplicity p n that replaces ⊤ by zero. n.factorization is of type ℕ →₀ ℕ and is defined in terms of padic_val_nat p n. All of them have some API.

So, based on these observations, it appears to me that padic_val_nat is the canonical choice, but I would like to have some input on that.

[Kevin Buzzard]

I've always worked on the hypothesis that padic_val_nat should be the one which should be developed, and similarly I think there's padic_val_int and padic_val_rat which I would be happy to argue were the canonical spellings.

[Kevin Buzzard]

This is only for additive valuations though, for multiplicative valuations hopefully there's something else.

[Michael Stoll]

I have a version of the final theorem that avoids valuations altogether:

lemma nat.eq_sq_add_sq_iff_eq_sq_mul {n : ℕ} :
  (∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∃ a b : ℕ, n = a ^ 2 * b ∧ is_square (-1 : zmod b) := ...

But the more standard way of stating it should of course be there.
In any case, thanks @Kevin Buzzard for your input!

[Michael Stoll]

There is some API missing around squarefree and padic_val_nat. There is, e.g., docs#nat.squarefree.factorization_le_one and docs#multiplicity.squarefree_iff_multiplicity_le_one, but apparently nothing relating to padic_val_nat(neither "squarefree padic" nor "padic squarefree" in the search window turns up anything).

[Michael Stoll]

#19054 is the PR that adds the characterization which natural numbers are sums of two squares.