Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.factorial_factorization_eq_div

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1034 to 1051

Source documentation

For primes p > √n, the p-adic valuation of n! equals ⌊n/p⌋. This follows from Legendre's formula since p² > n implies all higher power terms vanish.

Exact Lean statement

lemma Params.initial.factorial_factorization_eq_div {n p : ℕ} (hp : p.Prime)
    (h_sqrt : p > Real.sqrt n) :
    (n.factorial).factorization p = n / p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.factorial_factorization_eq_div {n p : ℕ} (hp : p.Prime)    (h_sqrt : p > Real.sqrt n) :    (n.factorial).factorization p = n / p := by  have h_legendre : (factorial n).factorization p =      ∑ k ∈ Finset.Ico 1 (log p n + 1), n / p ^ k := by    rw [factorization_def]    · have := Fact.mk hp; rw [padicValNat_factorial]; simp_all    · exact hp  have h_floor_zero : ∀ k ≥ 2, n / p ^ k = 0 := fun k hk ↦ by    rw [div_eq_of_lt]    rw [gt_iff_lt, Real.sqrt_lt (Nat.cast_nonneg n) (Nat.cast_nonneg p)] at h_sqrt    norm_cast at *    nlinarith [Nat.pow_le_pow_right hp.one_lt.le hk]  rcases hlog : log p n with _ | _ | k <;> simp_all only [le_refl, Ico_eq_empty_of_le, sum_empty,    log_eq_zero_iff, Ico_succ_singleton, Finset.sum_singleton, pow_one, Nat.div_eq_zero_iff]  · rw [div_eq_of_lt (hlog.resolve_right hp.one_lt.not_ge)]  · cases h_floor_zero (‹_› + 2) (by linarith) <;> simp_all +decide [log_eq_iff]    grind