Commit 2026-03-21 08:07 fec83365

feat(Combinatorics/Graph): some small graphs (no edge, bouquet, banana) (#35905) This pull request adds new constructors and supporting lemmas for special types of graphs in the Mathlib/Combinatorics/Graph/Basic.lean file. It introduces:

• Graph.noEdge V: The graph with vertex set V and empty edge set.
• Graph.bouquet v E: The graph with vertex set {v} and edge set E, where all edges are loops at v.
• Graph.banana u v E: The graph with vertex set {u, v} and edge set E, where all edges connect u and v. along with various properties and characterizations for these graphs.