Theorems · Theorem · commutative algebra
Ring.choose_natCast
∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (n k : ℕ),
Ring.choose (↑n) k = ↑(n.choose k)- Defined in
- Mathlib.RingTheory.Binomial
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.factorialproof · cited by 616
- Nat.choosestatement and proof · cited by 494
- NonAssocRingstatement and proof · cited by 483
- nsmul_eq_mulproof · cited by 369
- Nat.cast_mulproof · cited by 309
- Polynomial.smevalproof · cited by 65
- Nat.factorial_ne_zeroproof · cited by 56
- NatPowAssocstatement and proof · cited by 53
- descPochhammerproof · cited by 51
- BinomialRingstatement and proof · cited by 46
- Ring.choosestatement · cited by 43
- nsmul_right_injproof · cited by 21
Cited by4
Results whose statement or proof uses this declaration.
- mahler_natCast_eqproof · cited by 2
- PowerSeries.binomialSeries_natproof · cited by 1
- Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 1
- PowerSeries.rescale_neg_one_invOneSubPowproof · cited by 0