English
For prime p, if k ≤ p^n, k ≠ 0, ν_p( C(p^n, k) ) = n − ν_p(k).
Русский
Для простого p: ν_p( C(p^n, k) ) = n − ν_p(k) при k ≤ p^n, k ≠ 0.
LaTeX
$$$ emultiplicity(p, (p^n).choose k) = n - emultiplicity(p, k) $$$
Lean4
theorem emultiplicity_choose_prime_pow_add_emultiplicity (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
emultiplicity p (choose (p ^ n) k) + emultiplicity p k = n :=
le_antisymm
(by
have hdisj :
Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k}) := by
simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
rw [emultiplicity_choose hp hkn (lt_succ_self _),
emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt (lt_succ_of_le (log_mono_right hkn)), ←
Nat.cast_add]
apply WithTop.coe_mono
rw [log_pow hp.one_lt, ← card_union_of_disjoint hdisj, filter_union_right]
have filter_le_Ico := (Ico 1 n.succ).card_filter_le fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
rwa [card_Ico 1 n.succ] at filter_le_Ico)
(by rw [← hp.emultiplicity_pow_self]; exact emultiplicity_le_emultiplicity_choose_add hp _ _)
