A nonzero integer as a power of p times a unit at p, and a square of this form

Candidates for Mathlib.NumberTheory.Padics.PadicVal.Basic: a nonzero integer as the power of p of its valuation times an integer prime to p, for any p ≠ 1 (Int.exists_eq_pow_padicValInt_mul), the p-adic valuation of the integer p ^ k for any p > 1 (padicValInt_base_pow, the integer form of padicValNat_base_pow), and a square that is a power of p times a unit at p, whose exponent is even and whose unit part is a square (Int.even_and_isSquare_of_sq_eq_pow_mul), also for a square that is a sum whose terms but one are divisible by a higher power of p (Int.even_and_exists_isSquare_add_of_sq_eq_sum).

Main statements

• Int.exists_eq_pow_padicValInt_mul: a nonzero integer is p ^ v_p(n) times an integer prime to p, for p ≠ 1.
• padicValInt_base_pow: v_p(p ^ k) = k for the integer p ^ k and p > 1.
• Int.even_and_isSquare_of_sq_eq_pow_mul: y ^ 2 = p ^ v u with p ∤ u makes v even and u a square.
• Int.even_and_exists_isSquare_add_of_sq_eq_sum: a square sum with one term p ^ v u of least valuation, p ∤ u, makes v even and u + p t a square for some t.

theorem Int.exists_eq_pow_padicValInt_mul {p : ℕ} (hp : p ≠ 1) {n : ℤ} (hn : n ≠ 0) : ∃ (r : ℤ), n = ↑p ^ padicValInt p n * r ∧ ¬↑p ∣ r

A nonzero integer is p ^ v_p(n) times an integer prime to p, for any p ≠ 1, since the multiplicity of p in n is finite (FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd).

theorem padicValInt_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) : padicValInt p (↑p ^ k) = k

theorem Int.even_and_isSquare_of_sq_eq_pow_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {y u : ℤ} {v : ℕ} (h : y ^ 2 = ↑p ^ v * u) (hu : ¬↑p ∣ u) : Even v ∧ IsSquare u

A square with a known power of p. If y ^ 2 = p ^ v u with p ∤ u, then v is even, by the valuations at p, and u is the square of y / p ^ (v / 2).

theorem Int.even_and_exists_isSquare_add_of_sq_eq_sum {ι : Type u_1} {s : Finset ι} {f : ι → ℤ} {p : ℕ} [Fact (Nat.Prime p)] {y u : ℤ} {v : ℕ} {j : ι} (hy : y ^ 2 = ∑ i ∈ s, f i) (hj : j ∈ s) (hfj : f j = ↑p ^ v * u) (hu : ¬↑p ∣ u) (h : ∀ i ∈ s, i ≠ j → ↑p ^ (v + 1) ∣ f i) : Even v ∧ ∃ (t : ℤ), IsSquare (u + ↑p * t)

A square sum with one term of least valuation. If y ^ 2 = ∑ i ∈ s, f i, where f j = p ^ v u with p ∤ u and p ^ (v + 1) divides every other term, then v is even and u + p t is a square for some t, so that u is a square modulo p.