Commit 2026-04-29 01:17 dab5a06e

View on Github →

chore(Combinatorics/SimpleGraph/Finite): golf (#38624)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.degree_le_maxDegree

modified theorem SimpleGraph.degree_lt_card_verts