2026-05-18 22:44
Mathlib/Combinatorics/SimpleGraph/Matching.lean
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API (#36451)
Added SimpleGraph.Subgraph.IsMatching.verts_eq_biUnion_edgeSet