Commit 2023-03-27 12:09 32663014

View on Github →

feat: port Combinatorics.SimpleGraph.Matching (#3071)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.Subgraph.IsMatching.even_card

added theorem SimpleGraph.Subgraph.IsMatching.support_eq_verts

added theorem SimpleGraph.Subgraph.IsMatching.toEdge.surjective

added theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj

added theorem SimpleGraph.Subgraph.IsMatching.toEdge_eq_toEdge_of_adj

added def SimpleGraph.Subgraph.IsMatching

added theorem SimpleGraph.Subgraph.IsPerfectMatching.even_card

added def SimpleGraph.Subgraph.IsPerfectMatching

added theorem SimpleGraph.Subgraph.isMatching_iff_forall_degree

added theorem SimpleGraph.Subgraph.isPerfectMatching_iff

added theorem SimpleGraph.Subgraph.isPerfectMatching_iff_forall_degree