Commit 2024-09-06 19:00 a4b56a06

View on Github →

feat(Combinatorics/SimpleGraph): add miscellaneous lemmas (#16294)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Dart.lean

added theorem SimpleGraph.Dart.fst_ne_snd

added theorem SimpleGraph.Dart.snd_ne_fst

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.getLast_darts_snd

added theorem SimpleGraph.Walk.getLast_support

added theorem SimpleGraph.Walk.head_darts_fst

added theorem SimpleGraph.Walk.head_support