Commit 2025-05-23 22:03 7ed4f813
View on Github →feat(Combinatorics/SimpleGraph/Finite): Add lemmas about min and max degrees (#25121) Add lemmas about the min and max degree for general and empty graphs. Refactor maxDegree_le_of_forall_degree_le using simp.