emultiplicity_le_emultiplicity_choose_add

English

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

Русский

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

LaTeX

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

Lean4

/-- A lower bound on the multiplicity of `p` in `choose n k`. -/
theorem emultiplicity_le_emultiplicity_choose_add {p : ℕ} (hp : p.Prime) :
    ∀ n k : ℕ, emultiplicity p n ≤ emultiplicity p (choose n k) + emultiplicity p k
  | _, 0 => by simp
  | 0, _ + 1 => by simp
  | n + 1, k + 1 => by
    rw [← hp.emultiplicity_mul]
    refine emultiplicity_le_emultiplicity_of_dvd_right ?_
    rw [← succ_mul_choose_eq]
    exact dvd_mul_right _ _

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