graph theory PRs

Stream: graph theory

[Johan Commelin]

Hey all (@Alena Gusakov @Kyle Miller @Aaron Anderson @Bhavik Mehta @Jalex Stark). I'm happy to see some graph theory PRs coming in. But I'm not really a graph theory expert, and I don't have a good vision for what the library should look like. I also don't have the time to become an expert :wink:
So, here's my proposal for these PRs: I will try my best to review them. But it would be very useful if you would also thoroughly review each others PRs. If you approve the PR (using the github review feature), then I will see those green checkmarks, and feel a lot more comfortable.
(Of course this means that you shouldn't give that green checkmark too hastily. I will interpret it as a statement that you don't have any comments or remarks left, and are happy with the way the PR looks like.)

[Johan Commelin]

That said, some general advice: (i) There are many other formalisation libraries out there on graph theory. Don't forget to take inspiration from those. (And I know some of you have already been doing this.)
(ii) Try to aim for some well-known (but not too hard) results in graph theory. Reaching such targets is good evidence that you are creating a useful library with a good API.

[Alena Gusakov]

Sorry about that! I think I just saw your name in some files when I was working on other PRs and wasn't paying attention to which ones they were, so in my mind I associated your name with the graph theory stuff

[Alena Gusakov]

The matching/perfect matching definitions are working toward Hall's Marriage Theorem and later Tutte's theorem

[Johan Commelin]

Alena Gusakov said:

Sorry about that! I think I just saw your name in some files when I was working on other PRs and wasn't paying attention to which ones they were, so in my mind I associated your name with the graph theory stuff

No worries. I don't mind getting pinged.

[Jalex Stark]

Johan Commelin said:

(ii) Try to aim for some well-known (but not too hard) results in graph theory. Reaching such targets is good evidence that you are creating a useful library with a good API.

I think Alena and Bhavik are pushing on Hall's marriage theorem, hoping to get it working in a non-mathlib project in time for the exp. math deadline?

[Alena Gusakov]

yeah Bhavik and Kyle are helping out

[Alena Gusakov]

once i'm done with my brute-force proof i'll clean it up and start slicing off into PRs