English
If p is prime and k ≤ p^n, k ≠ 0, then (p^n choose k).factorization p + k.factorization p = n.
Русский
Если p — простое, k ≤ p^n, k ≠ 0, тогда (p^n choose k).factorization p + k.factorization p = n.
LaTeX
$$$ (p^n \\choose k).factorization p + k.factorization p = n. $$$
Lean4
theorem factorization_choose_prime_pow_add_factorization (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
(choose (p ^ n) k).factorization p + k.factorization p = n :=
by
apply le_antisymm
· 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 [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
rw [factorization_choose hp hkn (lt_succ_self _),
factorization_eq_card_pow_dvd_of_lt hp hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt),
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
· nth_rewrite 1 [← factorization_pow_self (n := n) hp]
exact factorization_le_factorization_choose_add hkn hk0
