English
The set of p^k for k up to padicValNat p n is contained in the divisors of n, for n ≠ 0.
Русский
Множество p^k для k до v_p(n) содержится в делителях n, при n ≠ 0.
LaTeX
$$$\\forall p,n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow (\\operatorname{Finset.range}(\\operatorname{padicValNat} p n + 1)).image(p^{\\cdot}) \\subseteq n.divisors$$$
Lean4
/-- **Kummer's Theorem**
Taking (`p - 1`) times the `p`-adic valuation of the binomial `n + k` over `k` equals the sum of the
digits of `k` plus the sum of the digits of `n` minus the sum of digits of `n + k`, all base `p`.
-/
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {k n : ℕ} [hp : Fact p.Prime] :
(p - 1) * padicValNat p (choose (n + k) k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum :=
by
have h : k ≤ n + k := by exact Nat.le_add_left k n
simp only [Nat.choose_eq_factorial_div_factorial h]
rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]
simp only [sub_one_mul_padicValNat_factorial]
rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <| digit_sum_le p n,
Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq, add_comm,
tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add (digit_sum_le p n) (digit_sum_le p k)),
Nat.sub_self (k + n), zero_add, add_comm]
