sub_one_mul_factorization_factorial

English

For a prime p, (p − 1) times the p-adic exponent of n! equals n minus the sum of base-p digits of n.

Русский

Для простого p, (p−1) раз показатель p в n! равен n минус сумма цифр n в осн. p.

LaTeX

$$$ (p-1) \\cdot (n)!.factorization p = n - (p.digits n).sum. $$$

Lean4

/-- For a prime number `p`, taking `(p - 1)` times the factorization of `p` in `n!` equals `n` minus
the sum of base `p` digits of `n`. -/
theorem sub_one_mul_factorization_factorial {n p : ℕ} (hp : p.Prime) :
    (p - 1) * (n)!.factorization p = n - (p.digits n).sum := by
  simp only [factorization_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]

Похожие утверждения