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

State before:
m : ℕ
⊢ mchoose m 0 = 1
Tactic:
simp only [mchoose, MulZeroClass.mul_zero, Nat.choose_self, Finset.prod_const_one]
State after:
no goals