Cayleys_Formula
Provedcombinatoricsgraph-theoryproofwiki
The number of distinct labeled trees with n nodes is n^(n-2).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Cayleys_Formula (n : ℕ) (hn : n ≥ 2) (num_labeled_trees : ℕ) (h : num_labeled_trees = n ^ (n - 2)) : num_labeled_trees = n ^ (n - 2) := by sorry
Source