Commit 2024-08-12 13:06 58d29b1d

View on Github →

feat(Combinatorics/SimpleGraph/Matching): Add matching free graphs (#15357) Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.IsMatchingFree.mono

added def SimpleGraph.IsMatchingFree

added theorem SimpleGraph.exists_maximal_isMatchingFree

Modified Mathlib/Data/Fintype/Order.lean

added theorem Finite.exists_ge_minimal

added theorem Finite.exists_le_maximal