Commit 2025-02-13 09:11 4083b7d9
View on Github →feat(Combinatorics/SimpleGraph): add monotonicity of number of odd components (#20398)
adds SimpleGraph.odd_components_card_mono and SimpleGraph.odd_components_card_deleteVerts_mono along with supporting lemma's.
In addition, migrate from Nat.card to Set.ncard where appropriate.
In preparation for Tutte's theorem.