Commit 2024-08-15 22:11 c98ad2f6

View on Github →

feat(Combinatorics/SimpleGraph): Define diameter of simple graphs and provide basic lemmas related to it (#12058) This defines the diameter of a simple graph, and provides a basic API for it.

Estimated changes

added theorem SimpleGraph.diam_bot
added theorem SimpleGraph.diam_def
added theorem SimpleGraph.diam_top
added theorem SimpleGraph.ediam_anti
added theorem SimpleGraph.ediam_bot
added theorem SimpleGraph.ediam_def
added theorem SimpleGraph.ediam_top