Theorem: Imo1987P1.main₀ (Compfiles/Imo1987P1.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ ∑ k ∈ range (n + 1), k * p (Fin n) k = n * (n - 1)!
Tactic:
simpa using main_fintype (Fin n)
State after:
no goals