Theorems · Theorem · number theory
Choose.choose_modEq_choose_mod_mul_choose_div
∀ {n k p : ℕ} [Fact (Nat.Prime p)], ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]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_nat for the version with MOD.
- Defined in
- Mathlib.Data.Nat.Choose.Lucas
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites52
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringproof · cited by 13,802
- Polynomialproof · cited by 5,681
- Finset.sumproof · cited by 5,195
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Factstatement and proof · cited by 2,726
- Finset.sum_congrproof · cited by 2,323
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.Primestatement and proof · cited by 2,059
- SProd.sprodproof · cited by 1,750
- mul_assocproof · cited by 1,667
Cited by2
Results whose statement or proof uses this declaration.
- Choose.choose_mul_mul_modEq_chooseproof · cited by 2
- Choose.choose_modEq_choose_mod_mul_choose_div_natproof · cited by 0