English
For a prime p and natural n, (p − 1) · ν_p(n!) = n − s_p(n), where s_p(n) is the sum of base-p digits of n.
Русский
Для простого p и n выполняется (p−1)·ν_p(n!) = n − s_p(n), где s_p(n) — сумма цифр числа n в основании p.
LaTeX
$$$ (p - 1) \cdot emultiplicity(p, n!) = n - s_p(n) $, где $s_p(n)$ — сумма цифр числа n в системе оснований p$$
Lean4
/-- 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 {n p : ℕ} (hp : p.Prime) :
(p - 1) * multiplicity p n ! = n - (p.digits n).sum := by
simp only [multiplicity_eq_of_emultiplicity_eq_some <|
emultiplicity_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]
