key₁ — Mathlib

English

For prime p, and n,i,j with j < p^n, the p-adic power p^{n - v_p(j+1)} divides the binomial coefficient (p^n choose j+1).

Русский

Для простого p и индексов n,i,j с j < p^n, число p^{n - v_p(j+1)} делит биномиальный коэффициент (p^n choose j+1).

LaTeX

$$$\forall (n,j) \; (hj : j < p^n) \Rightarrow p^{n - v_p(j+1)} \mid {p^n \choose j+1}.$$$

Lean4

/-- A key divisibility fact for the proof of `WittVector.map_frobeniusPoly`. -/
theorem key₁ (n j : ℕ) (hj : j < p ^ n) : p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1) :=
  by
  apply pow_dvd_of_le_emultiplicity
  rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]

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