diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean
index 4fc6a972b04d8..e27bbf65c3096 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean
@@ -203,7 +203,7 @@ abbrev Hom :=
   RelHom G.Adj G'.Adj
 
 /-- A graph embedding is an embedding `f` such that for vertices `v w : V`,
-`G.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'.
+`G'.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'.
 
 The notation `G ↪g G'` represents the type of graph embeddings. -/
 abbrev Embedding :=