Commit 2025-02-17 05:53 0dfd8207

View on Github →

feat(SimpleGraph/Finite): add degree_le_of_le minDegree_eq_zero and minDegree_le_minDegree (#21268)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.degree_le_of_le

added theorem SimpleGraph.minDegree_le_minDegree

added theorem SimpleGraph.minDegree_of_isEmpty