Commit 2025-03-20 16:17 0cdc26bc

View on Github →

feat(Combinatorics/SimpleGraph): define odd components (#22125) Adds the definition oddComponents: The set of connected components of odd cardinality. In preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

deleted theorem SimpleGraph.ConnectedComponent.odd_card_supp_iff_odd_subcomponents

added theorem SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp

added theorem SimpleGraph.ncard_oddComponents_mono

deleted theorem SimpleGraph.ncard_odd_components_mono

deleted theorem SimpleGraph.odd_card_iff_odd_components

added theorem SimpleGraph.odd_ncard_oddComponents

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean