choose_modEq_choose_mod_mul_choose_div_nat

English

Let p be a prime. For all n,k, C(n,k) ≡ C(n mod p, k mod p) · C(n/p, k/p) (MOD p).

Русский

Пусть p — простое. Для любых n,k: C(n,k) ≡ C(n mod p, k mod p) · C(n/p, k/p) (MOD p).

LaTeX

$$$ \\binom{n}{k} \\equiv \\binom{n \\bmod p}{k \\bmod p} \\cdot \\binom{n / p}{k / p} \\ [\\mathrm{MOD}\\ p]. $$$

Lean4

/-- For primes `p`, `choose n k` is congruent to `choose (n % p) (k % p) * choose (n / p) (k / p)`
modulo `p`. Also see `choose_modEq_choose_mod_mul_choose_div` for the version with `ZMOD`. -/
theorem choose_modEq_choose_mod_mul_choose_div_nat :
    choose n k ≡ choose (n % p) (k % p) * choose (n / p) (k / p) [MOD p] :=
  by
  rw [← Int.natCast_modEq_iff]
  exact_mod_cast choose_modEq_choose_mod_mul_choose_div

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