Skip to content

Commit c151f2d

Browse files
committed
remove redundant simp
1 parent da743eb commit c151f2d

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,6 @@ theorem colorable_one_iff : G.Colorable 1 ↔ G = ⊥ := by
185185
/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
186186
This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
187187
the original graph `G` and considering every color class (independent set) as a single vertex. -/
188-
@[simps!]
189188
abbrev Coloring.homMap {α : Type*} (f : G.Coloring α) : G →g G.map f :=
190189
.map f G f.map_adj
191190

0 commit comments

Comments
 (0)