English
For a prime p, ν_p(p(n+1))! = ν_p(p n)! + ν_p(n+1) + 1.
Русский
Для простого p: ν_p((p(n+1))!) = ν_p((pn)!) + ν_p(n+1) + 1.
LaTeX
$$$ emultiplicity(p, (p (n + 1))!) = emultiplicity(p, (p n)!) + emultiplicity(p, (n + 1)) + 1 $$$
Lean4
/-- 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 emultiplicity_factorial_mul_succ {n p : ℕ} (hp : p.Prime) :
emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1 :=
by
have hp' := hp.prime
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 hm : emultiplicity p (p * n)! ≠ ⊤ :=
by
rw [Ne, emultiplicity_eq_top, Classical.not_not, Nat.finiteMultiplicity_iff]
exact ⟨hp.ne_one, factorial_pos _⟩
revert hm
have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0 :=
by
intro m hm
rw [emultiplicity_eq_zero, not_dvd_iff_lt_mul_succ _ hp.pos]
rw [mem_Ico] at hm
exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
simp_rw [← prod_Ico_id_eq_factorial, Finset.emultiplicity_prod hp', ← sum_Ico_consecutive _ h1 h3, add_assoc]
intro h
rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self, sum_congr rfl h4,
sum_const_zero, zero_add, add_comm 1]
