Mathlib Changelog
v4
Changelog
About
Github
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