From b38ccad38abdf50ab1521d125446b847ce1628e5 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Thu, 14 Sep 2023 20:43:46 +0200 Subject: [PATCH] more fixes for review comments --- Mathlib/Data/Nat/Multiplicity.lean | 8 +++++--- Mathlib/NumberTheory/Padics/PadicVal.lean | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean index 8c3757139a511b..986a9659a47192 100644 --- a/Mathlib/Data/Nat/Multiplicity.lean +++ b/Mathlib/Data/Nat/Multiplicity.lean @@ -24,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 +122,8 @@ 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 diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean index 0bd6833f72678f..f10d58666d8380 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 @@ -597,7 +597,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]