Commit 2024-07-17 20:33 0df982c9

View on Github →

chore(Combinatorics/SimpleGraph): Change girth to egirth and introduce Nat-valued girth (#13910) Makes statements about girth more natural, for example, turns ENat.toNat G.girth ≤ 2 * G.diam + 1 to G.girth ≤ 2 * G.diam + 1.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Girth.lean

added theorem SimpleGraph.egirth_anti

added theorem SimpleGraph.egirth_bot

added theorem SimpleGraph.egirth_eq_top

added theorem SimpleGraph.exists_egirth_eq_length

modified theorem SimpleGraph.girth_anti

modified theorem SimpleGraph.girth_bot

deleted theorem SimpleGraph.girth_eq_top

added theorem SimpleGraph.girth_eq_zero

added theorem SimpleGraph.le_egirth

deleted theorem SimpleGraph.le_girth

added theorem SimpleGraph.three_le_egirth

modified theorem SimpleGraph.three_le_girth