Commit 2024-07-26 11:21 7f05fec7

View on Github →

feat({Algebra/BigOperators,Combinatorics/SimpleGraph}): Odd cardinality of odd components (#14623) Added lemma to prove a graph on an odd number of nodes has an odd number of odd components, including supporting lemmas. In preparation for Tuttes theorem

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Ring/Nat.lean

added theorem Finset.even_sum_iff_even_card_odd

added theorem Finset.odd_sum_iff_odd_card_odd

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.iUnion_connectedComponentSupp

added theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent

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

added theorem SimpleGraph.odd_card_iff_odd_components

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.toFinset_iUnion