Commit 2023-09-04 20:25 02e140cb

View on Github →

feat: Girth of a simple graph (#6948) Define the girth of a simple graph as a ℕ∞.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.isAcyclic_bot

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.IsCycle.ne_bot

Created Mathlib/Combinatorics/SimpleGraph/Girth.lean

added theorem SimpleGraph.exists_girth_eq_length

added theorem SimpleGraph.girth_anti

added theorem SimpleGraph.girth_bot

added theorem SimpleGraph.girth_eq_top

added theorem SimpleGraph.le_girth