Commit 2024-08-04 11:42 16631a09

View on Github →

refactor(Combinatorics/SimpleGraph): remove sndOfNotNil in favour of getVert 1 (#15237) This allows to leave out the not-nil hypothesis, in addition to not needing it for the definition of tail.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

modified theorem SimpleGraph.Walk.IsPath.tail

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.adj_getVert_one

deleted theorem SimpleGraph.Walk.adj_sndOfNotNil

deleted theorem SimpleGraph.Walk.cons_getVert

deleted theorem SimpleGraph.Walk.cons_getVert_succ

deleted theorem SimpleGraph.Walk.cons_sndOfNotNil

modified theorem SimpleGraph.Walk.cons_tail_eq

added def SimpleGraph.Walk.drop

added theorem SimpleGraph.Walk.getVert_cons

added theorem SimpleGraph.Walk.getVert_cons_one

added theorem SimpleGraph.Walk.getVert_cons_succ

added theorem SimpleGraph.Walk.getVert_copy

deleted theorem SimpleGraph.Walk.getVert_one

modified theorem SimpleGraph.Walk.getVert_tail

added theorem SimpleGraph.Walk.not_nil_iff_lt_length

deleted def SimpleGraph.Walk.sndOfNotNil

modified theorem SimpleGraph.Walk.support_tail

added theorem SimpleGraph.Walk.support_tail_of_not_nil

modified def SimpleGraph.Walk.tail

added theorem SimpleGraph.Walk.tail_cons_eq

added theorem SimpleGraph.Walk.tail_cons_nil

deleted theorem SimpleGraph.Walk.tail_support_eq_support_tail