Theorems · Theorem · number theory

Nat.castChoose_eq

∀ {A : Type u_1} [inst : CommSemiring A] {m : ℕ} {k : ℕ × ℕ},
  IsUnit ↑m.factorial →
    k ∈ Finset.HasAntidiagonal.antidiagonal m →
      ↑(m.choose k.1) = ↑m.factorial * Ring.inverse ↑k.1.factorial * Ring.inverse ↑k.2.factorial

Defined in: Mathlib.Data.Nat.Factorial.NatCast
Cited by: 1 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement · cited by 13,712
CommSemiringstatement and proof · cited by 10,911
IsUnitstatement and proof · cited by 1,602
add_commproof · cited by 1,535
Nat.factorialstatement and proof · cited by 616
Nat.choosestatement and proof · cited by 494
Nat.cast_mulproof · cited by 309
Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
Ring.inversestatement and proof · cited by 160
Finset.HasAntidiagonal.mem_antidiagonalproof · cited by 51
Nat.add_choose_mul_factorial_mul_factorialproof · cited by 5
Ring.eq_mul_inverse_iff_mul_eqproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

DividedPowers.OfInvertibleFactorial.dpow_add_of_ltproof · cited by 1