Theorem: mchoose_zero (DividedPowers/ForMathlib/CombinatoricsLemmas.lean)

State before:
n : ℕ
⊢ mchoose 0 n = 1
Tactic:
rw [mchoose, Finset.range_zero, Finset.prod_empty]
State after:
no goals