factorization_choose_prime_pow — Mathlib

English

For p prime, 0 < k ≤ p^n, and k ≠ 0, the p-adic exponent in C(p^n, k) equals n − k.factorization p.

Русский

Если p простое, 0<k ≤ p^n, и k ≠ 0, то показатель p в C(p^n, k) равен n − k.factorization p.

LaTeX

$$$ (p^n \\choose k).factorization p = n - k.factorization p. $$$

Lean4

theorem factorization_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
    (choose (p ^ n) k).factorization p = n - k.factorization p :=
  by
  nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]
  rw [Nat.add_sub_cancel_right]

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