Cycle of given length

Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.CycleLength

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Combinatorics.SimpleGraph.Paths

/-! # Cycle of given length -/

namespace Conjectura.GraphTheory

/-- A graph **has a cycle of length `k`** when some closed walk of that length repeats no
vertex or edge. Which cycle lengths a graph must contain is the subject of a large family of
extremal questions. -/
def HasCycleLength {V : Type*} (G : SimpleGraph V) (k : ℕ) : Prop :=
  ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = k

end Conjectura.GraphTheory