Commit 2025-03-28 14:56 f48bc9d3

feat(SimpleGraph): a connected graph with n - 1 edges is a tree (#23399) We prove that a connected graph on n vertices and n-1 edges is a tree, with a few API lemmas along the way, including the existence of spanning trees of connected graphs.
The large import is because we need some Minimal API. Invoking the existence of minimal/maximal objects in finite settings is standard in graph theory proofs, so this import should also be helpful with other things going forward.