Commit 2024-09-18 08:24 1cf58af1

View on Github →

feat(Combinatorics/SimpleGraph): add Fintype instance for Path (#13810)

Estimated changes

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

deleted theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq

added theorem SimpleGraph.coe_finsetWalkLengthLT_eq

added def SimpleGraph.finsetWalkLengthLT

added theorem SimpleGraph.mem_finsetWalkLengthLT_iff

added theorem SimpleGraph.mem_finsetWalkLength_iff