Commit 2024-11-29 09:51 8f06fcac

View on Github →

feat(Combinatorics/SimpleGraph/Matching): add IsCycles and IsAlternating with basic results (#19250) add SimpleGraph.IsCycles and SimpleGraph.IsAlternating with some basic results involving matchings. These are defined on SimpleGraph, because we want to use the symmDiff defined on there. This is in preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added def SimpleGraph.IsAlternating

added theorem SimpleGraph.IsCycles.other_adj_of_adj

added def SimpleGraph.IsCycles

added theorem SimpleGraph.IsPerfectMatching.symmDiff_spanningCoe_of_isAlternating

added theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_spanningCoe_IsCycles