Data.Nat.Choose.Basic: Register a faster implementation (#3915)

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
leanprover-community · Jun 29, 2023 · 3b028f2 · 3b028f2
1 parent 08133ab
commit 3b028f2
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -273,6 +273,14 @@ theorem choose_eq_descFactorial_div_factorial (n k : ℕ) : n.choose k = n.descF
   exact (Nat.mul_div_cancel' <| factorial_dvd_descFactorial _ _).symm
 #align nat.choose_eq_desc_factorial_div_factorial Nat.choose_eq_descFactorial_div_factorial
 
+/-- A faster implementation of `choose`, to be used during bytecode evaluation
+and in compiled code. -/
+def fast_choose n k := Nat.descFactorial n k / Nat.factorial k
+
+@[csimp] lemma choose_eq_fast_choose : Nat.choose = fast_choose :=
+  funext (fun _ => funext (Nat.choose_eq_descFactorial_div_factorial _))
+
+
 /-! ### Inequalities -/