Theorem SimpleGraph.degree_le_of_le

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