English
For prime p, and hkn:hkn: k ≤ p^n, hk0: k ≠ 0, ν_p( C(p^n, k) ) + ν_p(k) = n.
Русский
Для простого p и k ≤ p^n, k ≠ 0: ν_p( C(p^n, k) ) + ν_p(k) = n.
LaTeX
$$$ emultiplicity(p, (p^n).choose k) + emultiplicity(p, k) = n $$$
Lean4
/-- The multiplicity of `p` in `choose (n + k) k` is the number of carries when `k` and `n`
are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
is any bound greater than `log p (n + k)`. -/
theorem emultiplicity_choose' {p n k b : ℕ} (hp : p.Prime) (hnb : log p (n + k) < b) :
emultiplicity p (choose (n + k) k) = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) :=
by
have h₁ :
emultiplicity p (choose (n + k) k) + emultiplicity p (k ! * n !) =
#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + emultiplicity p (k ! * n !) :=
by
rw [← hp.emultiplicity_mul, ← mul_assoc]
have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt (add_comm n k ▸ hnb)),
multiplicity_choose_aux hp (le_add_left k n)]
simp [add_comm]
refine WithTop.add_right_cancel ?_ h₁
apply finiteMultiplicity_iff_emultiplicity_ne_top.1
exact Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩
