lean_workbook_plus_795
Openis odd tells us is odd.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_795 (n : ℕ) (h : n ≠ 0) : Odd (choose n 1) → Odd n := by sorry
Source
is odd tells us is odd.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_795 (n : ℕ) (h : n ≠ 0) : Odd (choose n 1) → Odd n := by sorry