α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ 1 / 1 = 1
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ multinomial ∅ f = 1
dsimp [multinomial]
no goals
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ 1 / 1 = 1
rfl