Commit 2026-06-02 20:46 12831fa3

View on Github →

chore(Combinatorics/SimpleGraph): tidy various files (#37642)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

added theorem SimpleGraph.Colorable.chromaticNumber_pos

deleted theorem SimpleGraph.chromaticNumber_pos

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

added theorem SimpleGraph.Copy.maxDegree_mono

deleted theorem SimpleGraph.Copy.max_degree_le

deleted theorem SimpleGraph.Copy.minDegree_le

added theorem SimpleGraph.Copy.minDegree_mono

deleted theorem SimpleGraph.Hom.minDegree_le

added theorem SimpleGraph.Hom.minDegree_mono

added theorem SimpleGraph.IsContained.maxDegree_mono

deleted theorem SimpleGraph.IsContained.max_degree_le

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

modified theorem SimpleGraph.incMatrix_mul_transpose

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

modified theorem SimpleGraph.Embedding.map_apply

modified theorem SimpleGraph.Iso.comap_apply

modified theorem SimpleGraph.Iso.map_apply

deleted def SimpleGraph.overFin

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

added theorem SimpleGraph.Walk.support_take

deleted theorem SimpleGraph.Walk.take_support_eq_support_take_succ

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Subwalks.lean