[Merged by Bors] - chore(Combinatorics/SimpleGraph): fix naming of colorable_iff_forall_connectedComponents

Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean

@@ -173,7 +173,7 @@ lemma two_colorable_iff_forall_loop_even {α : Type*} {G : SimpleGraph α} :
   · intro _ w ho
     have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le
     norm_cast
-  · apply colorable_iff_forall_connectedComponents.2
+  · apply colorable_iff_forall_connectedComponent.2
     intro c
     obtain ⟨_, hv⟩ := c.nonempty_supp
     use fun a ↦ Fin.ofNat 2 (c.connected_toSimpleGraph ⟨_, hv⟩ a).some.length

Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean

@@ -314,11 +314,14 @@ theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) :
       simp only [Fin.mk_eq_mk, Ne]
       exact C.valid hvw
 
-theorem colorable_iff_forall_connectedComponents {n : ℕ} :
+theorem colorable_iff_forall_connectedComponent {n : ℕ} :
     G.Colorable n ↔ ∀ c : G.ConnectedComponent, (c.toSimpleGraph).Colorable n :=
   ⟨fun ⟨C⟩ _ ↦ ⟨fun v ↦ C v, fun h h1 ↦ C.valid h h1⟩,
    fun h ↦ ⟨G.homOfConnectedComponents (fun c ↦ (h c).some)⟩⟩
 
+@[deprecated (since := "2026-07-12")]
+alias colorable_iff_forall_connectedComponents := colorable_iff_forall_connectedComponent
+
 theorem colorable_set_nonempty_of_colorable {n : ℕ} (hc : G.Colorable n) :
     { n : ℕ | G.Colorable n }.Nonempty :=
   ⟨n, hc⟩