Theorem SimpleGraph.minDegree_le_minDegree

Modification history

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_le_minDegree View on Github →