chore(GroupTheory): rename IsSolvable to Group.IsSolvable (leanprover-community#41820)

Renames `IsSolvable` to `Group.IsSolvable`.

Author: plp127

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -155,8 +155,8 @@ theorem not_solvable_by_rad (p : ℕ) (x : ℂ) (hx : aeval x (Φ ℚ a b) = 0)
   have h_irred := irreducible_Phi a b p hp hpa hpb hp2b
   apply mt (isSolvable_gal_of_irreducible · h_irred hx)
   intro h
-  refine Equiv.Perm.not_solvable _ (le_of_eq ?_)
-    (solvable_of_surjective (gal_Phi a b hab h_irred).2)
+  refine Equiv.Perm.not_isSolvable _ (le_of_eq ?_)
+    (Group.isSolvable_of_surjective (gal_Phi a b hab h_irred).2)
   rw_mod_cast [Cardinal.mk_fintype, complex_roots_Phi a b h_irred.separable]
 
 theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) : x ∉ solvableByRad ℚ ℂ := by

Mathlib/FieldTheory/AbelRuffini.lean

@@ -30,59 +30,60 @@ open Polynomial
 
 variable {F E : Type*} [Field F] [Field E] [Algebra F E]
 
-theorem gal_zero_isSolvable : IsSolvable (0 : F[X]).Gal := by infer_instance
+theorem gal_zero_isSolvable : Group.IsSolvable (0 : F[X]).Gal := by infer_instance
 
-theorem gal_one_isSolvable : IsSolvable (1 : F[X]).Gal := by infer_instance
+theorem gal_one_isSolvable : Group.IsSolvable (1 : F[X]).Gal := by infer_instance
 
-theorem gal_C_isSolvable (x : F) : IsSolvable (C x).Gal := by infer_instance
+theorem gal_C_isSolvable (x : F) : Group.IsSolvable (C x).Gal := by infer_instance
 
-theorem gal_X_isSolvable : IsSolvable (X : F[X]).Gal := by infer_instance
+theorem gal_X_isSolvable : Group.IsSolvable (X : F[X]).Gal := by infer_instance
 
-theorem gal_X_sub_C_isSolvable (x : F) : IsSolvable (X - C x).Gal := by infer_instance
+theorem gal_X_sub_C_isSolvable (x : F) : Group.IsSolvable (X - C x).Gal := by infer_instance
 
-theorem gal_X_pow_isSolvable (n : ℕ) : IsSolvable (X ^ n : F[X]).Gal := by infer_instance
+theorem gal_X_pow_isSolvable (n : ℕ) : Group.IsSolvable (X ^ n : F[X]).Gal := by infer_instance
 
-theorem gal_mul_isSolvable {p q : F[X]} (_ : IsSolvable p.Gal) (_ : IsSolvable q.Gal) :
-    IsSolvable (p * q).Gal :=
-  solvable_of_solvable_injective (Gal.restrictProd_injective p q)
+theorem gal_mul_isSolvable {p q : F[X]} (_ : Group.IsSolvable p.Gal) (_ : Group.IsSolvable q.Gal) :
+    Group.IsSolvable (p * q).Gal :=
+  Group.isSolvable_of_isSolvable_injective (Gal.restrictProd_injective p q)
 
-theorem gal_prod_isSolvable {s : Multiset F[X]} (hs : ∀ p ∈ s, IsSolvable (Gal p)) :
-    IsSolvable s.prod.Gal := by
+theorem gal_prod_isSolvable {s : Multiset F[X]} (hs : ∀ p ∈ s, Group.IsSolvable (Gal p)) :
+    Group.IsSolvable s.prod.Gal := by
   apply Multiset.induction_on' s
   · exact gal_one_isSolvable
   · intro p t hps _ ht
     rw [Multiset.insert_eq_cons, Multiset.prod_cons]
     exact gal_mul_isSolvable (hs p hps) ht
 
 theorem gal_isSolvable_of_splits {p q : F[X]}
-    (_ : Fact ((p.map (algebraMap F q.SplittingField)).Splits)) (hq : IsSolvable q.Gal) :
-    IsSolvable p.Gal :=
-  haveI : IsSolvable (q.SplittingField ≃ₐ[F] q.SplittingField) := hq
-  solvable_of_surjective (AlgEquiv.restrictNormalHom_surjective q.SplittingField)
+    (_ : Fact ((p.map (algebraMap F q.SplittingField)).Splits)) (hq : Group.IsSolvable q.Gal) :
+    Group.IsSolvable p.Gal :=
+  haveI : Group.IsSolvable (q.SplittingField ≃ₐ[F] q.SplittingField) := hq
+  Group.isSolvable_of_surjective (AlgEquiv.restrictNormalHom_surjective q.SplittingField)
 
 theorem gal_isSolvable_tower (p q : F[X]) (hpq : (p.map (algebraMap F q.SplittingField)).Splits)
-    (hp : IsSolvable p.Gal) (hq : IsSolvable (q.map (algebraMap F p.SplittingField)).Gal) :
-    IsSolvable q.Gal := by
+    (hp : Group.IsSolvable p.Gal)
+    (hq : Group.IsSolvable (q.map (algebraMap F p.SplittingField)).Gal) :
+    Group.IsSolvable q.Gal := by
   let K := p.SplittingField
   let L := q.SplittingField
   have : Fact ((p.map (algebraMap F L)).Splits) := ⟨hpq⟩
   let ϕ : Gal(L/K) ≃* (q.map (algebraMap F K)).Gal :=
     (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr
   have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
-  have : IsSolvable Gal(K/F) := hp
-  have : IsSolvable Gal(L/K) := solvable_of_solvable_injective ϕ_inj
+  have : Group.IsSolvable Gal(K/F) := hp
+  have : Group.IsSolvable Gal(L/K) := Group.isSolvable_of_isSolvable_injective ϕ_inj
   exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField
 
 section GalXPowSubC
 
 set_option backward.isDefEq.respectTransparency false in
-theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).Gal := by
+theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : Group.IsSolvable (X ^ n - 1 : F[X]).Gal := by
   by_cases hn : n = 0
   · rw [hn, pow_zero, sub_self]
     exact gal_zero_isSolvable
   have hn' : 0 < n := pos_iff_ne_zero.mpr hn
   have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
-  apply isSolvable_of_comm
+  apply Group.isSolvable_of_comm
   intro σ τ
   ext a ha
   simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha
@@ -96,7 +97,7 @@ theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).G
 
 set_option backward.isDefEq.respectTransparency false in
 theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
-    (h : ((X ^ n - 1 : F[X]).map (RingHom.id F)).Splits) : IsSolvable (X ^ n - C a).Gal := by
+    (h : ((X ^ n - 1 : F[X]).map (RingHom.id F)).Splits) : Group.IsSolvable (X ^ n - C a).Gal := by
   by_cases ha : a = 0
   · rw [ha, C_0, sub_zero]
     exact gal_X_pow_isSolvable n
@@ -114,7 +115,7 @@ theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
       (Splits.degree_eq_one_of_irreducible (h.of_dvd (map_ne_zero hn''')
         (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))
           (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))))
-  apply isSolvable_of_comm
+  apply Group.isSolvable_of_comm
   intro σ τ
   ext b hb
   rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb
@@ -172,7 +173,7 @@ theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [F
     hs', ← C_pow, hb, ← mul_assoc, C_mul_C, one_mul]
   rfl
 
-theorem gal_X_pow_sub_C_isSolvable (n : ℕ) (x : F) : IsSolvable (X ^ n - C x).Gal := by
+theorem gal_X_pow_sub_C_isSolvable (n : ℕ) (x : F) : Group.IsSolvable (X ^ n - C x).Gal := by
   by_cases hx : x = 0
   · rw [hx, C_0, sub_zero]
     exact gal_X_pow_isSolvable n
@@ -259,7 +260,7 @@ protected theorem solvableByRad.induction (motive : ∀ x, x ∈ solvableByRad F
   exact h
 
 private theorem induction_rad {x : E} (hx : x ∈ solvableByRad F E) {n : ℕ} (hn : n ≠ 0)
-    (hα : IsSolvable (minpoly F (x ^ n)).Gal) : IsSolvable (minpoly F x).Gal := by
+    (hα : Group.IsSolvable (minpoly F (x ^ n)).Gal) : Group.IsSolvable (minpoly F x).Gal := by
   let p := minpoly F (x ^ n)
   have hp : p.comp (X ^ n) ≠ 0 := by
     intro h
@@ -288,8 +289,8 @@ open IntermediateField
 
 private theorem induction_step {x y z : E}
     (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E) (hz : z ∈ solvableByRad F E)
-    (hx' : IsSolvable (minpoly F x).Gal) (hy' : IsSolvable (minpoly F y).Gal) (hz' : z ∈ F⟮x, y⟯) :
-    IsSolvable (minpoly F z).Gal := by
+    (hx' : Group.IsSolvable (minpoly F x).Gal) (hy' : Group.IsSolvable (minpoly F y).Gal)
+    (hz' : z ∈ F⟮x, y⟯) : Group.IsSolvable (minpoly F z).Gal := by
   let p := minpoly F x
   let q := minpoly F y
   have hpq := SplittingField.splits (p * q)
@@ -313,7 +314,7 @@ private theorem induction_step {x y z : E}
   infer_instance
 
 theorem isSolvable_gal_minpoly {x : E} (hx : x ∈ solvableByRad F E) :
-    IsSolvable (minpoly F x).Gal := by
+    Group.IsSolvable (minpoly F x).Gal := by
   induction hx using solvableByRad.induction with
   | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
   | add y z hy hz hy' hz' =>
@@ -328,11 +329,11 @@ alias solvableByRad.isSolvable := isSolvable_gal_minpoly
 /-- **Abel-Ruffini Theorem** (one direction): An irreducible polynomial with a `solvableByRad` root
 has a solvable Galois group. -/
 theorem isSolvable_gal_of_irreducible {x : E} (hx : x ∈ solvableByRad F E) {q : F[X]}
-    (q_irred : Irreducible q) (q_aeval : aeval x q = 0) : IsSolvable q.Gal := by
-  have : IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
+    (q_irred : Irreducible q) (q_aeval : aeval x q = 0) : Group.IsSolvable q.Gal := by
+  have : Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
     rw [minpoly.eq_of_irreducible q_irred q_aeval]
     exact isSolvable_gal_minpoly hx
-  refine solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)
+  refine Group.isSolvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)
   aesop
 
 @[deprecated (since := "2026-02-28")]

Mathlib/FieldTheory/Normal/Basic.lean

@@ -243,16 +243,16 @@ theorem Normal.minpoly_eq_iff_mem_orbit [h : Normal F E] {x y : E} :
 
 variable (F K₁)
 
-theorem isSolvable_of_isScalarTower [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)]
-    [h2 : IsSolvable (E ≃ₐ[K₁] E)] : IsSolvable Gal(E/F) := by
+theorem isSolvable_of_isScalarTower [Normal F K₁] [h1 : Group.IsSolvable (K₁ ≃ₐ[F] K₁)]
+    [h2 : Group.IsSolvable (E ≃ₐ[K₁] E)] : Group.IsSolvable Gal(E/F) := by
   let f : (E ≃ₐ[K₁] E) →* Gal(E/F) :=
     { toFun := fun ϕ =>
         AlgEquiv.ofAlgHom (ϕ.toAlgHom.restrictScalars F) (ϕ.symm.toAlgHom.restrictScalars F)
           (AlgHom.ext fun x => ϕ.apply_symm_apply x) (AlgHom.ext fun x => ϕ.symm_apply_apply x)
       map_one' := AlgEquiv.ext fun _ => rfl
       map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }
   refine
-    solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
+    Group.isSolvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
       ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩
   exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))
 

Mathlib/GroupTheory/IsPerfect.lean

@@ -82,7 +82,7 @@ lemma not_isNilpotent [Nontrivial G] [IsPerfect G] : ¬ IsNilpotent G :=
 open scoped IsMulCommutative in
 variable (G) in
 lemma not_isMulCommutative [Nontrivial G] [IsPerfect G] : ¬ IsMulCommutative G :=
-  fun _ ↦ (not_isSolvable G) CommGroup.isSolvable
+  fun _ ↦ (not_isSolvable G) inferInstance
 
 instance subsingleton_of_isMulCommutative
     [hG : IsPerfect G] [h_comm : IsMulCommutative G] : Subsingleton G := by

Mathlib/GroupTheory/Nilpotent.lean

@@ -1158,7 +1158,7 @@ theorem Group.nilpotencyClass_pi [Fintype η] [∀ i, IsNilpotent (Gs i)] :
 end FinitePi
 
 /-- A nilpotent subgroup is solvable -/
-instance (priority := 100) IsNilpotent.to_isSolvable [h : IsNilpotent G] : IsSolvable G := by
+instance (priority := 100) IsNilpotent.to_isSolvable [h : IsNilpotent G] : Group.IsSolvable G := by
   obtain ⟨n, hn⟩ := nilpotent_iff_lowerCentralSeries.1 h
   use n
   rw [eq_bot_iff, ← hn]

Mathlib/GroupTheory/Solvable.lean

@@ -101,31 +101,45 @@ section Solvable
 
 variable (G)
 
+namespace Group
+
 /-- A group `G` is solvable if its derived series is eventually trivial. We use this definition
   because it's the most convenient one to work with. -/
 @[mk_iff isSolvable_def, wikidata Q759832]
 class IsSolvable : Prop where
   /-- A group `G` is solvable if its derived series is eventually trivial. -/
   solvable : ∃ n : ℕ, derivedSeries G n = ⊥
 
-instance (priority := 100) CommGroup.isSolvable {G : Type*} [CommGroup G] : IsSolvable G :=
+@[deprecated (since := "2026-07-16")]
+alias _root_.IsSolvable := Group.IsSolvable
+
+@[deprecated (since := "2026-07-17")]
+alias _root_.isSolvable_def := Group.isSolvable_def
+
+instance (priority := 100) {G : Type*} [CommGroup G] : IsSolvable G :=
   ⟨⟨1, le_bot_iff.mp (Abelianization.commutator_subset_ker (MonoidHom.id G))⟩⟩
 
 theorem isSolvable_of_comm {G : Type*} [hG : Group G] (h : ∀ a b : G, a * b = b * a) :
     IsSolvable G := by
   let hG' : CommGroup G := { hG with mul_comm := h }
   cases hG
-  exact CommGroup.isSolvable
+  infer_instance
+
+@[deprecated (since := "2026-07-16")]
+alias _root_.isSolvable_of_comm := Group.isSolvable_of_comm
 
 theorem isSolvable_of_top_eq_bot (h : (⊤ : Subgroup G) = ⊥) : IsSolvable G :=
   ⟨⟨0, h⟩⟩
 
-instance (priority := 100) isSolvable_of_subsingleton [Subsingleton G] : IsSolvable G :=
+@[deprecated (since := "2026-07-16")]
+alias _root_.isSolvable_of_top_eq_bot := Group.isSolvable_of_top_eq_bot
+
+instance (priority := 100) [Subsingleton G] : IsSolvable G :=
   isSolvable_of_top_eq_bot G (by simp [eq_iff_true_of_subsingleton])
 
 variable {G}
 
-theorem solvable_of_ker_le_range {G' G'' : Type*} [Group G'] [Group G''] (f : G' →* G)
+theorem isSolvable_of_ker_le_range {G' G'' : Type*} [Group G'] [Group G''] (f : G' →* G)
     (g : G →* G'') (hfg : g.ker ≤ f.range) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] :
     IsSolvable G := by
   obtain ⟨n, hn⟩ := id hG''
@@ -138,23 +152,32 @@ theorem solvable_of_ker_le_range {G' G'' : Type*} [Group G'] [Group G''] (f : G'
       (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
   | succ m hm => exact commutator_le_map_commutator hm hm
 
-theorem solvable_of_solvable_injective (hf : Function.Injective f) [IsSolvable G'] :
+@[deprecated (since := "2026-07-16")]
+alias _root_.solvable_of_ker_le_range := isSolvable_of_ker_le_range
+
+theorem isSolvable_of_isSolvable_injective (hf : Function.Injective f) [IsSolvable G'] :
     IsSolvable G :=
-  solvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot hf).symm ▸ bot_le)
+  isSolvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot hf).symm ▸ bot_le)
+
+@[deprecated (since := "2026-07-16")]
+alias _root_.solvable_of_solvable_injective := isSolvable_of_isSolvable_injective
+
+instance (H : Subgroup G) [IsSolvable G] : IsSolvable H :=
+  isSolvable_of_isSolvable_injective H.subtype_injective
 
-instance subgroup_solvable_of_solvable (H : Subgroup G) [IsSolvable G] : IsSolvable H :=
-  solvable_of_solvable_injective H.subtype_injective
+theorem isSolvable_of_surjective (hf : Function.Surjective f) [IsSolvable G] : IsSolvable G' :=
+  isSolvable_of_ker_le_range f (1 : G' →* G) (f.range_eq_top_of_surjective hf ▸ le_top)
 
-theorem solvable_of_surjective (hf : Function.Surjective f) [IsSolvable G] : IsSolvable G' :=
-  solvable_of_ker_le_range f (1 : G' →* G) (f.range_eq_top_of_surjective hf ▸ le_top)
+@[deprecated (since := "2026-07-16")]
+alias _root_.solvable_of_surjective := isSolvable_of_surjective
 
-instance solvable_quotient_of_solvable (H : Subgroup G) [H.Normal] [IsSolvable G] :
+instance (H : Subgroup G) [H.Normal] [IsSolvable G] :
     IsSolvable (G ⧸ H) :=
-  solvable_of_surjective (QuotientGroup.mk'_surjective H)
+  isSolvable_of_surjective (QuotientGroup.mk'_surjective H)
 
-instance solvable_prod {G' : Type*} [Group G'] [IsSolvable G] [IsSolvable G'] :
+instance {G' : Type*} [Group G'] [IsSolvable G] [IsSolvable G'] :
     IsSolvable (G × G') :=
-  solvable_of_ker_le_range (MonoidHom.inl G G') (MonoidHom.snd G G') fun x hx =>
+  isSolvable_of_ker_le_range (MonoidHom.inl G G') (MonoidHom.snd G G') fun x hx =>
     ⟨x.1, Prod.ext rfl hx.symm⟩
 
 variable (G) in
@@ -168,17 +191,24 @@ theorem IsSolvable.commutator_lt_top_of_nontrivial [hG : IsSolvable G] [Nontrivi
   | zero => exact derivedSeries_zero G
   | succ n h => rwa [derivedSeries_succ, h]
 
+@[deprecated (since := "2026-07-16")]
+alias _root_.IsSolvable.commutator_lt_top_of_nontrivial :=
+  Group.IsSolvable.commutator_lt_top_of_nontrivial
+
 theorem IsSolvable.commutator_lt_of_ne_bot [IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) :
     ⁅H, H⁆ < H := by
   rw [← nontrivial_iff_ne_bot] at hH
   rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]
   exact commutator_lt_top_of_nontrivial H
 
+@[deprecated (since := "2026-07-16")]
+alias _root_.IsSolvable.commutator_lt_of_ne_bot := Group.IsSolvable.commutator_lt_of_ne_bot
+
 theorem isSolvable_iff_commutator_lt [WellFoundedLT (Subgroup G)] :
     IsSolvable G ↔ ∀ H : Subgroup G, H ≠ ⊥ → ⁅H, H⁆ < H := by
   refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
   suffices h : IsSolvable (⊤ : Subgroup G) from
-    solvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
+    isSolvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
   induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH
   rcases eq_or_ne H ⊥ with rfl | h'
   · infer_instance
@@ -193,6 +223,11 @@ theorem isSolvable_iff_commutator_lt [WellFoundedLT (Subgroup G)] :
         ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
     | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
 
+@[deprecated (since := "2026-07-16")]
+alias _root_.isSolvable_iff_commutator_lt := Group.isSolvable_iff_commutator_lt
+
+end Group
+
 end Solvable
 
 section IsSimpleGroup
@@ -208,8 +243,8 @@ theorem IsSimpleGroup.derivedSeries_succ {n : ℕ} : derivedSeries G n.succ = co
     · rw [h, commutator_bot_left]
     · rwa [h]
 
-theorem IsSimpleGroup.comm_iff_isSolvable : (∀ a b : G, a * b = b * a) ↔ IsSolvable G :=
-  ⟨isSolvable_of_comm, fun ⟨⟨n, hn⟩⟩ => by
+theorem IsSimpleGroup.comm_iff_isSolvable : (∀ a b : G, a * b = b * a) ↔ Group.IsSolvable G :=
+  ⟨Group.isSolvable_of_comm, fun ⟨⟨n, hn⟩⟩ => by
     cases n
     · intro a b
       refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
@@ -224,31 +259,40 @@ end IsSimpleGroup
 
 section PermNotSolvable
 
-theorem not_solvable_of_mem_derivedSeries {g : G} (h1 : g ≠ 1)
-    (h2 : ∀ n : ℕ, g ∈ derivedSeries G n) : ¬IsSolvable G :=
-  mt (isSolvable_def _).mp
+theorem not_isSolvable_of_mem_derivedSeries {g : G} (h1 : g ≠ 1)
+    (h2 : ∀ n : ℕ, g ∈ derivedSeries G n) : ¬Group.IsSolvable G :=
+  mt (Group.isSolvable_def _).mp
     (not_exists_of_forall_not fun n h =>
       h1 (Subgroup.mem_bot.mp ((congr_arg (g ∈ ·) h).mp (h2 n))))
 
-theorem Equiv.Perm.fin_5_not_solvable : ¬IsSolvable (Equiv.Perm (Fin 5)) := by
+@[deprecated (since := "2026-07-16")]
+alias not_solvable_of_mem_derivedSeries := not_isSolvable_of_mem_derivedSeries
+
+theorem Equiv.Perm.not_isSolvable_fin_5 : ¬Group.IsSolvable (Equiv.Perm (Fin 5)) := by
   let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
   let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
   let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
   have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
-  refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
+  refine not_isSolvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
   induction n with
   | zero => exact mem_top x
   | succ n ih =>
     rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
     exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
 
-theorem Equiv.Perm.not_solvable (X : Type*) (hX : 5 ≤ Cardinal.mk X) :
-    ¬IsSolvable (Equiv.Perm X) := by
+@[deprecated (since := "2026-07-16")]
+alias Equiv.Perm.fin_5_not_solvable := Equiv.Perm.not_isSolvable_fin_5
+
+theorem Equiv.Perm.not_isSolvable (X : Type*) (hX : 5 ≤ Cardinal.mk X) :
+    ¬Group.IsSolvable (Equiv.Perm X) := by
   intro h
   have key : Nonempty (Fin 5 ↪ X) := by
     rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
   exact
-    Equiv.Perm.fin_5_not_solvable
-      (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))
+    Equiv.Perm.not_isSolvable_fin_5 (Group.isSolvable_of_isSolvable_injective
+      (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))
+
+@[deprecated (since := "2026-07-16")]
+alias Equiv.Perm.not_solvable := Equiv.Perm.not_isSolvable
 
 end PermNotSolvable