Commit 2026-05-21 10:51 c87cc975

feat(Combinatorics/SimpleGraph/Walk): make p.Nil the simpNF of p = nil and p.length = 0 (#39218) These are equivalent, and p.Nil works even when the endpoints of the walk aren't defeq. [#graph theory > Deprecate `p = nil` in favor of `p.Nil`?](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Deprecate.20.60p.20.3D.20nil.60.20in.20favor.20of.20.60p.2ENil.60.3F/with/538017334) The main event is Walk/Basic.lean:

• Swapped sides of nil_iff_eq_nil to create eq_nil_iff_nil, tagged @[simp] and deprecated the original
• Changed the RHS of length_eq_zero_iff from p = nil to p.Nil, and generalized to non-closed walks
• Deprecated nil_iff_length_eq which is the symmetric iff
• Added Nil.length_eq_zero alias
• Untagged exists_length_eq_zero_iff with @[simp] and added exists_nil_iff to replace it The rest is fixing everything that broke (or uses of now-deprecated lemmas), and:
• [Walk/Maps] Added nil_map_iff to replace map_eq_nil_iff which is the same but with .Nil instead of = nil
• [Walk/Decomp] Added nil_rotate to replace rotate_eq_nil which is the same but with .Nil instead of = nil