Skip to content

Commit 32343e7

Browse files
committed
un-namespace EdgeColoring.ofColor{Embedding/Iso} to get dot-notation on graphs
1 parent 23d1413 commit 32343e7

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

  • Mathlib/Combinatorics/SimpleGraph/Coloring

Mathlib/Combinatorics/SimpleGraph/Coloring/Edge.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -112,17 +112,17 @@ theorem chromaticIndex_eq_zero : G.chromaticIndex = 0 ↔ G = ⊥ := by
112112

113113
/-- Lift an embedding of colors to an embedding of edge colorings. -/
114114
@[expose]
115-
def EdgeColoring.ofColorEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=
115+
def edgeColoringEmbeddingofColorEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=
116116
recolorOfEmbedding _ f
117117

118118
/-- Lift an isomorphism of colors to an isomorphism of edge colorings. -/
119119
@[expose]
120-
def EdgeColoring.ofColorIso (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=
120+
def edgeColoringEquivOfColorIso (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=
121121
recolorOfEquiv _ f
122122

123123
@[gcongr]
124124
theorem EdgeColorableWith.mono (f : α ↪ β) (h : G.EdgeColorableWith α) : G.EdgeColorableWith β :=
125-
.ofColorEmbedding f h.some⟩
125+
edgeColoringEmbeddingofColorEmbedding f h.some⟩
126126

127127
@[gcongr]
128128
theorem EdgeColorable.mono (hle : n ≤ m) (h : G.EdgeColorable n) : G.EdgeColorable m :=

0 commit comments

Comments
 (0)