From 245441b73c057e0359c27b5ca7babba3a8660544 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <moritz.firsching@gmail.com>
Date: Fri, 15 Sep 2023 08:05:10 +0000
Subject: [PATCH] feat(Data.Nat.Multiplicity):
 sub_one_mul_multiplicity_factorial (#6546)

Co-authored-by: Moritz Firsching <firsching@google.com>
---
 Mathlib/Data/Nat/Multiplicity.lean        | 17 ++++++++++++++---
 Mathlib/NumberTheory/Padics/PadicVal.lean |  4 ++--
 2 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index a659617bd730fe..657a2811a75c7e 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -9,6 +9,7 @@ import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Log
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Digits
 import Mathlib.RingTheory.Multiplicity
 
 #align_import data.nat.multiplicity from "leanprover-community/mathlib"@"ceb887ddf3344dab425292e497fa2af91498437c"
@@ -23,9 +24,9 @@ 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`. See `padicValNat_factorial` for this
-  result stated in the language of `p`-adic valuations and
-  `sub_one_mul_padicValNat_factorial_eq_sub_sum_digits` for a related result.
+  `n / p + ... + n / p ^ b` for any `b` such that `n / p ^ (b + 1) = 0`. See `padicValNat_factorial`
+  for this result stated in the language of `p`-adic valuations and
+  `sub_one_mul_padicValNat_factorial` for a related result.
 * `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
@@ -122,6 +123,16 @@ theorem multiplicity_factorial {p : ℕ} (hp : p.Prime) :
         congr_arg _ <| Finset.sum_congr rfl fun _ _ => (succ_div _ _).symm
 #align nat.prime.multiplicity_factorial Nat.Prime.multiplicity_factorial
 
+/-- For a prime number `p`, taking `(p - 1)` times the multiplicity of `p` in `n!` equals `n` minus
+the sum of base `p` digits of `n`. -/
+ theorem sub_one_mul_multiplicity_factorial {p : ℕ} (hp : p.Prime) :
+     (p - 1) * (multiplicity p n !).get (finite_nat_iff.mpr ⟨hp.ne_one, factorial_pos n⟩) =
+     n - (p.digits n).sum := by
+  simp only [multiplicity_factorial hp <| lt_succ_of_lt <| lt.base (log p n),
+      ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range,
+      ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]
+  rfl
+
 /-- The multiplicity of `p` in `(p * (n + 1))!` is one more than the sum
   of the multiplicities of `p` in `(p * n)!` and `n + 1`. -/
 theorem multiplicity_factorial_mul_succ {n p : ℕ} (hp : p.Prime) :
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index c6186e5cb15a57..eaf0f53e780c01 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -39,7 +39,7 @@ quotients `n / p ^ i`. This sum is expressed over the finset `Ico 1 b` where `b`
 greater than `log p n`. See `Nat.Prime.multiplicity_factorial` for the same result but stated in the
 language of prime multiplicity.
 
-* `sub_one_mul_padicValNat_factorial_eq_sub_sum_digits`: Legendre's Theorem.  Taking (`p - 1`) times
+* `sub_one_mul_padicValNat_factorial`: Legendre's Theorem.  Taking (`p - 1`) times
 the `p`-adic valuation of `n!` equals `n` minus the sum of base `p` digits of `n`.
 
 * `padicValNat_choose`: Kummer's Theorem. The `p`-adic valuation of `n.choose k` is the number
@@ -603,7 +603,7 @@ theorem padicValNat_factorial {n b : ℕ} [hp : Fact p.Prime] (hnb : log p n < b
 
 Taking (`p - 1`) times the `p`-adic valuation of `n!` equals `n` minus the sum of base `p` digits
 of `n`. -/
-theorem sub_one_mul_padicValNat_factorial_eq_sub_sum_digits [hp : Fact p.Prime] (n : ℕ):
+theorem sub_one_mul_padicValNat_factorial [hp : Fact p.Prime] (n : ℕ):
     (p - 1) * padicValNat p (n !) = n - (p.digits n).sum := by
   rw [padicValNat_factorial <| lt_succ_of_lt <| lt.base (log p n), ← Finset.sum_Ico_add' _ 0 _ 1,
     Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]