noncomputable def Nat.factorial (n : Nat) : Nat

Equations

• n.factorial = Nat.prod_ft 0 n fun (i : Nat) => i + 1

@[simp]

theorem Nat.factorial_zero : Nat.factorial 0 = 1

@[simp]

theorem Nat.factorial_succ {n : Nat} : (n + 1).factorial = n.factorial * (n + 1)

@[simp]

theorem Nat.factorial_pos {n : Nat} : 0 < n.factorial

theorem Nat.factorial_monotone : Monotone Nat.factorial

theorem Nat.factorial_lt_succ {n : Nat} : (n + 1).factorial < (n + 1 + 1).factorial

theorem Nat.factorial_strictMono : StrictMonotone fun (n : Nat) => (n + 1).factorial

noncomputable def Nat.binom (n k : Nat) : Nat

Equations

• n.binom k = if k ≤ n then n.factorial / (k.factorial * (n - k).factorial) else 0

@[simp]

theorem Nat.binom_zero_of_gt {n k : Nat} : n < k → n.binom k = 0

@[simp]

theorem Nat.binom_of_le {n k : Nat} : k ≤ n → n.binom k = n.factorial / (k.factorial * (n - k).factorial)