Theorem SimpleGraph.maxDegree_of_isEmpty

Modification history

2026-06-23 12:20

Mathlib/Combinatorics/SimpleGraph/Finite.lean

feat(Combinatorics/SimpleGraph/Finite): some `minDegree`/`maxDegree` lemmas (#40622) …

Deleted SimpleGraph.maxDegree_of_isEmpty View on Github →

2025-05-23 22:03

Mathlib/Combinatorics/SimpleGraph/Finite.lean

feat(Combinatorics/SimpleGraph/Finite): Add lemmas about min and max degrees (#25121) …

Added SimpleGraph.maxDegree_of_isEmpty View on Github →