A numerical diagonal sum in Pascal’s triangle
ProvedWorkbookRestored.plus_8968lean-workbookrestored-importssource-checked
The binomial coefficients satisfy
This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_8968 (Apache-2.0).
Preamble
import Mathlib.Data.Nat.Choose.Basic open Nat
Formal statement
theorem WorkbookRestored.plus_8968 : choose 3 0 + choose 4 1 + choose 5 2 = choose 6 2 := by sorry
Source