Commit 2025-04-30 12:12 5b76dec8

feat(Combinatorics/SimpleGraph): part of Tutte's theorem (#22119) Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's:

• necessity of the Tutte condition (not_isTutteViolator)
• the fact that the empty set violates the Tutte condition if the number of vertices is odd (IsTutteViolator.empty)
• the construction of a perfect matching in a graph that decomposes into cliques (Subgraph.IsPerfectMatching.exists_of_isClique_supp) Definitions added: IsTutteViolator.