feat(NumberTheory/Padics/PadicVal): padicValNat_factorial (#5802)

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

Author: mo271

Mathlib/Data/Nat/Multiplicity.lean

@@ -23,7 +23,8 @@ coefficients.
 ## Multiplicity calculations
 
 * `Nat.Prime.multiplicity_factorial`: Legendre's Theorem. The multiplicity of `p` in `n!` is
-  `n/p + ... + n/p^b` for any `b` such that `n/p^(b + 1) = 0`.
+  `n/p + ... + n/p^b` for any `b` such that `n/p^(b + 1) = 0`. See `padicValNat_factorial` for the
+  for this result stated in the language of `p`-adic valuations.
 * `Nat.Prime.multiplicity_factorial_mul`: The multiplicity of `p` in `(p * n)!` is `n` more than
   that of `n!`.
 * `Nat.Prime.multiplicity_choose`: Kummer's Theorem. The multiplicity of `p` in `n.choose k` is the

Mathlib/NumberTheory/Padics/PadicVal.lean

@@ -33,12 +33,16 @@ by taking `[Fact p.Prime]` as a type class argument.
 
 ## Calculations with `p`-adic valuations
 
+* `padicValNat_factorial`: Legendre's Theorem. The `p`-adic valuation of `n!` is the sum of the
+quotients `n / p ^ i`. This sum is expressed over the finset `Ico 1 b` where `b` is any bound
+greater than `log p n`. See `Nat.Prime.multiplicity_factorial` for the same result but stated in the
+language of prime multiplicity.
+
 * `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]
@@ -554,6 +558,20 @@ 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
 
+/-- **Legendre's Theorem**
+
+The `p`-adic valuation of `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed
+over the finset `Ico 1 b` where `b` is any bound greater than `log p n`. -/
+theorem padicValNat_factorial {p n b : ℕ} [hp : Fact p.Prime] (hnb : log p n < b) :
+    padicValNat p (n !) = ∑ i in Finset.Ico 1 b, n / p ^ i :=
+  PartENat.natCast_inj.mp ((padicValNat_def' (Nat.Prime.ne_one hp.out) <| factorial_pos _) ▸
+      Prime.multiplicity_factorial hp.out hnb)
+
+/-- **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`. -/
 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 :=