Commit 2026-03-18 23:07 de8a06c8

View on Github →

chore(Combinatorics/SimpleGraph): move WalkDecomp and WalkCounting to Walks (#36819) These lived in Connectivity probably because Walk was meant to live there. Split WalkCounting into Walks.Counting for anything that doesn't mention reachability, and Connectivity.Finite for anything that does.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Created Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean

added theorem SimpleGraph.ConnectedComponent.card_le_card_of_le

added theorem SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp

added theorem SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset

added theorem SimpleGraph.ncard_oddComponents_mono

added theorem SimpleGraph.odd_ncard_oddComponents

added theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty

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

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

Renamed Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean to Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean

deleted theorem SimpleGraph.ConnectedComponent.card_le_card_of_le

deleted theorem SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp

deleted theorem SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset

deleted theorem SimpleGraph.ncard_oddComponents_mono

deleted theorem SimpleGraph.odd_ncard_oddComponents

deleted theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty

Renamed Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean to Mathlib/Combinatorics/SimpleGraph/Walks/Decomp.lean