Add docstring

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -633,6 +633,8 @@ def overFin (hc : Fintype.card V = n) : SimpleGraph (Fin n) where
 noncomputable def overFinIso (hc : Fintype.card V = n) : G ≃g G.overFin hc := by
   use Fintype.equivFinOfCardEq hc; simp [overFin]
 
+/-- The isomorphism between `completeBipartiteGraph α β` and
+`completeBipartiteGraph (Fin s) (Fin t)` where `card α = s` and `card β = t`. -/
 noncomputable def completeBipartiteGraph.overFinIso {α β : Type*} [Fintype α] [Fintype β]
     {s t : ℕ} (hc₁ : Fintype.card α = s) (hc₂ : Fintype.card β = t) :
     completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) where