Commit 2025-05-15 18:38 358193a6

View on Github →

feat(Combinatorics/SimpleGraph): Tutte's theorem (#22915) Proves Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.not_isClique_iff

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

deleted theorem SimpleGraph.IsPerfectMatching.isAlternating_symmDiff_left

deleted theorem SimpleGraph.IsPerfectMatching.isAlternating_symmDiff_right

deleted theorem SimpleGraph.IsPerfectMatching.symmDiff_of_isAlternating

added theorem SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_left

added theorem SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_right

added theorem SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

added theorem SimpleGraph.edge_le_iff

modified theorem SimpleGraph.sup_edge_self

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

modified theorem SimpleGraph.IsTutteViolator.empty

added theorem SimpleGraph.IsTutteViolator.mono

added theorem SimpleGraph.exists_isTutteViolator

added theorem SimpleGraph.tutte

Modified docs/1000.yaml