lean_workbook_plus_51564
OpenIllustrate that represents choosing 0 things, which can only be done in 1 way
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51564 : ∀ n : ℕ, choose n 0 = 1 := by sorry
Source
Illustrate that represents choosing 0 things, which can only be done in 1 way
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_51564 : ∀ n : ℕ, choose n 0 = 1 := by sorry