Theorem SimpleGraph.diam_ne_zero_of_ediam_ne_top

Modification history

2025-03-28 02:52

Mathlib/Combinatorics/SimpleGraph/Diam.lean

feat(Combinatorics/SimpleGraph/Diam): add basic (e)diam facts (#23264) …

Added SimpleGraph.diam_ne_zero_of_ediam_ne_top View on Github →