feat(NumberTheory/Padics/PadicVal): factorial_choose (#5862)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib/Data/Nat/Multiplicity.lean

@@ -26,8 +26,9 @@ coefficients.
   `n/p + ... + n/p^b` for any `b` such that `n/p^(b + 1) = 0`.
 * `Nat.Prime.multiplicity_factorial_mul`: The multiplicity of `p` in `(p * n)!` is `n` more than
   that of `n!`.
-* `Nat.Prime.multiplicity_choose`: The multiplicity of `p` in `n.choose k` is the number of carries
-   when `k` and`n - k` are added in base `p`.
+* `Nat.Prime.multiplicity_choose`: Kummer's Theorem. The multiplicity of `p` in `n.choose k` is the
+   number of carries  when `k` and `n - k` are added in base `p`. See `padicValNat_choose` for the
+   same result but stated in the language of `p`-adic valuations.
 
 ## Other declarations
 

Mathlib/NumberTheory/Padics/PadicVal.lean

@@ -12,7 +12,7 @@ import Mathlib.Tactic.IntervalCases
 #align_import number_theory.padics.padic_val from "leanprover-community/mathlib"@"60fa54e778c9e85d930efae172435f42fb0d71f7"
 
 /-!
-# p-adic Valuation
+# `p`-adic Valuation
 
 This file defines the `p`-adic valuation on `ℕ`, `ℤ`, and `ℚ`.
 
@@ -31,6 +31,14 @@ This file uses the local notation `/.` for `Rat.mk`.
 Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
 by taking `[Fact p.Prime]` as a type class argument.
 
+## Calculations with `p`-adic valuations
+
+* `padicValNat_choose`: Kummer's Theorem. The `p`-adic valuation of `n.choose k` is the number
+of carries when `k` and `n - k` are added in base `p`. This sum is expressed over the finset
+`Ico 1 b` where `b` is any bound greater than `log p n`. See `Nat.Prime.multiplicity_choose` for the
+same result but stated in the language of prime multiplicity.
+
+
 ## References
 
 * [F. Q. Gouvêa, *p-adic numbers*][gouvea1997]
@@ -546,6 +554,12 @@ theorem padicValNat_factorial_mul {p : ℕ} (n : ℕ) (hp : p.Prime):
       padicValNat_def' (Nat.Prime.ne_one hp) <| factorial_pos n]
   exact Prime.multiplicity_factorial_mul hp
 
+theorem padicValNat_choose {p n k b : ℕ} [hp : Fact p.Prime] (hkn : k ≤ n) (hnb : log p n < b) :
+    padicValNat p (choose n k) =
+    ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card :=
+  PartENat.natCast_inj.mp <| (padicValNat_def' (Nat.Prime.ne_one hp.out) <| choose_pos hkn) ▸
+  Prime.multiplicity_choose hp.out hkn hnb
+
 end padicValNat
 
 section padicValInt