lean_workbook_plus_40829
OpenIs it possible that whenever ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40829 (n j : ℕ) (h₁ : 2 * j + 1 > n) : choose n (2 * j + 1) = 0 := by sorry
Source
Is it possible that whenever ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_40829 (n j : ℕ) (h₁ : 2 * j + 1 > n) : choose n (2 * j + 1) = 0 := by sorry