Walk.IsChordless live in mathlib?

Stream: mathlib4

[tianyi zhao]

Hi all, I’m preparing a PR adding two definitions for simple graph walks:

def Walk.IsChord (p : G.Walk u u) (v w : V) : Prop :=
  v ∈ p.support ∧ w ∈ p.support ∧ G.Adj v w ∧ s(v, w) ∉ p.edges

def Walk.IsChordless (p : G.Walk u u) : Prop :=
  p.IsCycle ∧
    ∀ ⦃v w : V⦄, v ∈ p.support → w ∈ p.support → G.Adj v w → s(v, w) ∈ p.edges

I’m unsure about file placement:
1) Mathlib/Combinatorics/SimpleGraph/Paths.lean
2) a new file (e.g. ...)

Given current mathlib organization, where would you prefer these definitions to live?
If placement is agreed, I’ll open a draft PR with only these defs + minimal lemmas.

[Floris van Doorn]

I haven't worked much on graph theory, so maybe wait until someone more experienced chimes in (cc @Kyle Miller), but I think it makes sense to create a new file Mathlib.Combinatorics.SimpleGraph.Walks.Chords or similar.

[Floris van Doorn]

(I'm surprised that Paths.lean is not in the Walks subfolder)

[tianyi zhao]

Alright, thank you for your reply and for the very reasonable suggestion. I’ll wait for input from more experienced contributors, since I’ve never submitted a PR to mathlib before and I want to avoid harming mathlib’s high-quality files and code structure.