sub_one_mul_padicValNat_choose_eq_sub_sum_digits

English

The image of p^{t+1} for t in range(padicValNat p n) lies in n.divisors.erase 1.

Русский

Образ p^{t+1} для t в диапазоне v_p(n) лежит в n.divisors.erase 1.

LaTeX

$$$\\forall p,n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow ((\\operatorname{Finset.range}(\\operatorname{padicValNat} p n)).image (p^{(t+1)})) \\subseteq n.divisors.erase 1$$$

Lean4

/-- **Kummer's Theorem**
Taking (`p - 1`) times the `p`-adic valuation of the binomial `n` over `k` equals the sum of the
digits of `k` plus the sum of the digits of `n - k` minus the sum of digits of `n`, all base `p`.
-/
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {k n : ℕ} [hp : Fact p.Prime] (h : k ≤ n) :
    (p - 1) * padicValNat p (choose n k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum :=
  by
  convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_›
  all_goals cutsat

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