Theorems · Theorem · combinatorics
Nat.cast_choose
∀ (K : Type u_1) [inst : DivisionSemiring K] [CharZero K] {a b : ℕ},
a ≤ b → ↑(b.choose a) = ↑b.factorial / (↑a.factorial * ↑(b - a).factorial)- Defined in
- Mathlib.Data.Nat.Choose.Cast
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionSemiringCharZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_assocproof · cited by 1,667
- LT.lt.ne'proof · cited by 1,417
- CharZerostatement and proof · cited by 932
- Nat.factorialstatement and proof · cited by 616
- Nat.choosestatement and proof · cited by 494
- DivisionSemiringstatement and proof · cited by 216
- mul_ne_zeroproof · cited by 178
- Nat.cast_ne_zeroproof · cited by 113
- Nat.factorial_posproof · cited by 99
- eq_div_iff_mul_eqproof · cited by 19
- Nat.choose_mul_factorial_mul_factorialproof · cited by 13
Cited by6
Results whose statement or proof uses this declaration.
- UpperHalfPlane.qExpansion_mulproof · cited by 1
- norm_iteratedFDerivWithin_comp_le_auxproof · cited by 1
- Nat.cast_add_chooseproof · cited by 1
- Polynomial.hasseDeriv_compproof · cited by 0
- Numbering.dens_prefixedproof · cited by 0
- Polynomial.bernoulli_generating_functionproof · cited by 0