emultiplicity_choose_prime_pow — Mathlib

English

For prime p, with k ≤ p^n and k ≠ 0, ν_p( C(p^n, k) ) = n − multiplicity p k.

Русский

Для простого p: ν_p( C(p^n, k) ) = n − ν_p(k) при k ≤ p^n, k ≠ 0.

LaTeX

$$$ emultiplicity(p, (p^n).choose k) = n - multiplicity(p, k) $$$

Lean4

theorem emultiplicity_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
    emultiplicity p (choose (p ^ n) k) = ↑(n - multiplicity p k) :=
  by
  push_cast
  rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]
  norm_cast
  rw [Nat.add_sub_cancel_right]

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