English
Let p be prime. Then (p(n+1))! has p-adic exponent equal to the sum of the p-adic exponents of (pn)! and (n+1)! plus 1:
Русский
Пусть p — простое. Тогда v_p((p(n+1))!) = v_p((pn)!) + v_p((n+1)!) + 1.
LaTeX
$$$ (p \\cdot (n+1))!.factorization p = (p\\cdot n)!.factorization p + (n+1).factorization p + 1. $$$
Lean4
/-- The factorization of `p` in `(p * (n + 1))!` is one more than the sum of the factorizations of
`p` in `(p * n)!` and `n + 1`. -/
theorem factorization_factorial_mul_succ {n p : ℕ} (hp : p.Prime) :
(p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1 :=
by
have h0 : 2 ≤ p := hp.two_le
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by omega
have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 :=
by
apply factorization_eq_zero_of_not_dvd
exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right
rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt (mem_Ico.mp hx).left), ←
sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2, ← prod_Ico_id_eq_factorial,
factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt (mem_Ico.mp hx).left),
factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm, coe_add, Pi.add_apply, hp.factorization_self,
sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
