Commit 2026-04-23 08:52 67bc64ef

View on Github →

feat(Combinatorics/SimpleGraph/Copy): maxDegree is monotonic, and minDegree is monotonic over a surjective Copy (#38355)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

added theorem SimpleGraph.Copy.minDegree_le

added theorem SimpleGraph.Hom.minDegree_le

added theorem SimpleGraph.maxDegree_mono