p-adic valuation of product of powered prime numbers

Stream: mathlib4

[Gaëtan Serré]

I was formalizing some result on countability and I ended up proving that, for two prime numbers $p$ and $q$

$$\nu_p(p^n q^m) = n \\ \nu_q(p^n q^m) = m$$

The proof uses an intermediate lemma stating that

$$\nu_p(q^m) = 0$$

lemma intermediate {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n : ℕ) (h_neq : q ≠ p) : padicValNat q (p^n) = 0 :=
by
  have coprime_pow := Nat.Coprime.pow 1 n (Nat.coprime_pow_primes 1 1 hq.elim hp.elim h_neq)
  rewrite [show (q^1)^1 = q by simp, show p^1 = p by simp] at coprime_pow
  exact padicValNat.eq_zero_of_not_dvd ((Nat.Prime.coprime_iff_not_dvd hq.elim).mp coprime_pow)

theorem prod_pow_primes_left {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n m: ℕ) (h_neq : p ≠ q) : padicValNat p (p^n * q^m) = n := by
  rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm, padicValNat.prime_pow _, intermediate _ h_neq, add_zero]

theorem prod_pow_primes_right {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n m: ℕ) (h_neq : q ≠ p) : padicValNat q (p^n * q^m) = m := by
  rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm, padicValNat.prime_pow _, intermediate _ h_neq, zero_add]

Is this result exists already in Mathlib (maybe in a different formulation) and, if not, would it be an interesting one to add?

[Michael Stoll]

You can probably combine docs#padicValNat_primes, docs#padicValNat.pow, docs#padicValNat.mul and docs#padicValNat.prime_pow to get what you want.

[Filippo A. E. Nuccio]

When working with the $p$-adic valuation you might also want to inspect docs#IsDedekindDomain.HeightOneSpectrum.valuation, that benefits of the full valuation API in Mathlib.

[Gaëtan Serré]

Michael Stoll said:

You can probably combine docs#padicValNat_primes, docs#padicValNat.pow, docs#padicValNat.mul and docs#padicValNat.prime_pow to get what you want.

Thanks, I achieved getting rid of the intermediate lemma and Coprime stuff. The resulting proofs look like that

theorem prod_pow_primes_left {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
  (n m : ℕ) (neq : p ≠ q) : padicValNat p (p^n * q^m) = n := by
  rw [padicValNat.mul (NeZero.ne' (p^n)).symm (NeZero.ne' (q^m)).symm]
  have padic_p_pn_eq_n : padicValNat p (p^n) = n := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hp.elim), padicValNat_self, mul_one]
  have padic_p_qm_eq_0 : padicValNat p (q ^ m) = 0 := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hq.elim), padicValNat_primes neq, mul_zero]
  rw [padic_p_pn_eq_n, padic_p_qm_eq_0, add_zero]

theorem prod_pow_primes_right {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
  (n m : ℕ) (neq : q ≠ p) : padicValNat q (p^n * q^m) = m := by
  rw [padicValNat.mul (NeZero.ne' (p^n)).symm (NeZero.ne' (q^m)).symm]
  have padic_q_qm_eq_m : padicValNat q (q^m) = m := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hq.elim), padicValNat_self, mul_one]
  have padic_q_pn_eq_0 : padicValNat q (p ^ n) = 0 := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hp.elim), padicValNat_primes neq, mul_zero]
  rw [padic_q_qm_eq_m, padic_q_pn_eq_0, zero_add]

I guess that these results can be used to prove similar things on products of "powered" primes of arbitrary size by induction.

[Gaëtan Serré]

Filippo A. E. Nuccio said:

When working with the $p$-adic valuation you might also want to inspect docs#IsDedekindDomain.HeightOneSpectrum.valuation, that benefits of the full valuation API in Mathlib.

Indeed, I think it can be useful. However, it's getting too abstract for me...

[Michael Stoll]

You did not use docs#padicValNat.prime_pow, which gives you one of the haves for free.

[Gaëtan Serré]

Oh! Indeed, I was too focus on docs#padicValNat.pow. Thank you for noticing.

theorem prod_pow_primes_left {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
  (n m : ℕ) (neq : p ≠ q) : padicValNat p (p^n * q^m) = n := by
  rw [padicValNat.mul (NeZero.ne' (p^n)).symm (NeZero.ne' (q^m)).symm]
  have padic_p_qm_eq_0 : padicValNat p (q ^ m) = 0 := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hq.elim), padicValNat_primes neq, mul_zero]
  rw [padicValNat.prime_pow, padic_p_qm_eq_0, add_zero]

theorem prod_pow_primes_right {p q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
  (n m : ℕ) (neq : q ≠ p) : padicValNat q (p^n * q^m) = m := by
  rw [padicValNat.mul (NeZero.ne' (p^n)).symm (NeZero.ne' (q^m)).symm]
  have padic_q_pn_eq_0 : padicValNat q (p ^ n) = 0 := by
    rw [padicValNat.pow _ (Nat.Prime.ne_zero hp.elim), padicValNat_primes neq, mul_zero]
  rw [padicValNat.prime_pow, padic_q_pn_eq_0, zero_add]