Theorem SimpleGraph.minDegree_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.minDegree_of_isEmptyView on Github →
2025-02-17 05:53
Mathlib/Combinatorics/SimpleGraph/Finite.lean
feat(SimpleGraph/Finite): add degree_le_of_le minDegree_eq_zero and minDegree_le_minDegree (#21268)
Added SimpleGraph.minDegree_of_isEmptyView on Github →