Theorems · Definition · combinatorics
SimpleGraph.girth
{α : Type u_1} → SimpleGraph α → ℕThe girth of a simple graph is the length of its smallest cycle, or junk value 0 if the graph is
acyclic.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Girth
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- ENat.toNatproof · cited by 143
- SimpleGraph.egirthproof · cited by 17
Cited by11
Results whose statement or proof uses this declaration.
- SimpleGraph.three_le_girthstatement · cited by 1
- SimpleGraph.girth_eq_zerostatement and proof · cited by 1
- SimpleGraph.exists_girth_eq_lengthstatement and proof · cited by 0
- SimpleGraph.IsContained.girth_lestatement · cited by 0
- SimpleGraph.Walk.IsCircuit.girth_le_lengthstatement · cited by 0
- SimpleGraph.Iso.girth_eqstatement · cited by 0
- SimpleGraph.girth_antistatement · cited by 0
- SimpleGraph.girth_botstatement · cited by 0
- SimpleGraph.girth_le_lengthstatement · cited by 0
- SimpleGraph.girth_topstatement · cited by 0
- SimpleGraph.IsAcyclic.girth_eq_zerostatement · cited by 0