Theorem SimpleGraph.ediam_le_two_mul_eccent

Modification history

2026-02-26 22:22

Mathlib/Combinatorics/SimpleGraph/Diam.lean

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

Added SimpleGraph.ediam_le_two_mul_eccent View on Github →