feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): add docstring to toSubgraph

SnirBroshi · SnirBroshi · commit 8736628f60c3 · 2025-10-05T10:06:31.000+03:00
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
@@ -125,6 +125,7 @@ namespace ConnectedComponent
 
 variable (C : G.ConnectedComponent)
 
+/-- The induced subgraph of a connected component. -/
 def toSubgraph : G.Subgraph :=
   Subgraph.induce ⊤ C.supp
 
