Commit 2026-02-26 22:22 2fff1442

View on Github →

feat(Combinatorics/SimpleGraph/Diam): drop Finite α from ediam_le_two_mul_radius (#33764)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

added theorem SimpleGraph.ediam_eq_top_iff_radius_eq_top

added theorem SimpleGraph.ediam_le_two_mul_eccent

modified theorem SimpleGraph.ediam_le_two_mul_radius