A binomial coefficient as a factorial quotient

Proved

WorkbookRestored.plus_24728

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

$\binom{14}{2}=14!/(12!2!)$ , with the quotient interpreted rationally.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_24728 (Apache-2.0).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Factorial.Basic
open Nat

Formal statement

theorem WorkbookRestored.plus_24728 : (choose 14 2 : ℚ) = (factorial 14)/(factorial 12 * factorial 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_24728; original Prove2Me node 41949601-14d5-451e-8618-898326d6ea24; Apache-2.0

View graph