dvd_choose_pow_iff — Mathlib

English

Let p be a prime and n, k natural numbers. Then p divides (p^n choose k) if and only if k ≠ 0 and k ≠ p^n.

Русский

Пусть p — простое число и n, k натуральны. Тогда p делит биномиальный коэффициент C(p^n, k) тогда и только тогда, когда k ≠ 0 и k ≠ p^n.

LaTeX

$$$\operatorname{Prime}(p) \Rightarrow \Big(p \mid \binom{p^n}{k} \iff k \neq 0 \land k \neq p^n\Big)$$$

Lean4

theorem dvd_choose_pow_iff (hp : Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n := by
  refine ⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩ <;> rintro rfl <;> simp [hp.ne_one] at h

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