Commit 2025-11-04 06:00 30d4cdf5

feat(SimpleGraph): Hall's Marriage Theorem for bipartite graphs (#29164) Derive the graph theoretic proof of Hall's marriage theorem from the combinatorial version. Note that I specifically implement this for the more general case of infinite graphs that are locally finite (e.g. every vertex has only finite neighbors.) As a result, the theorem depends on some category theoretic infrastructure required for the infinite combinatorial formulation of Hall's Marriage Theorem and hence I've placed the theorems into their own file to avoid requiring it in Matching.lean

• depends on: #29162