lean_workbook_plus_6115
ProvedProve that the binomial coefficient is an integer.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6115 (n r : ℕ) : ∃ k, k = n.choose r := by sorry
Source
Prove that the binomial coefficient is an integer.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6115 (n r : ℕ) : ∃ k, k = n.choose r := by sorry