Perfect matching

Stream: Is there code for X?

[Yaël Dillies]

Do we have perfect matchings in a branch or anywhere else? I want them in a general graph, not in a bipartite one as for Hall.
cc @Kyle Miller

[Kyle Miller]

docs#simple_graph.matching.is_perfect is for general graphs

There was an attempt at more of an API here https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/matching.lean