Number_of_Edges_in_Forest
Provedforestsgraph-theoryproofwiki
Let F be a forest with n nodes and m components. Then F contains n - m edges.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Number_of_Edges_in_Forest (n m edges : ℕ) (hm : m ≤ n) (h : edges = n - m) : edges = n - m := by sorry
Source