feat(GroupTheory): Add some results about derivedSeries (#25342)

Prove `Antitone (derivedSeries G)` and `(derivedSeries G n).Characteristic`.

Author: pelicanhere

Mathlib/GroupTheory/Abelianization.lean

@@ -56,6 +56,10 @@ theorem Subgroup.map_subtype_commutator (H : Subgroup G) :
     (_root_.commutator H).map H.subtype = ⁅H, H⁆ := by
   rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
 
+variable {G} in
+theorem Subgroup.commutator_le_self (H : Subgroup G) : ⁅H, H⁆ ≤ H :=
+  H.map_subtype_commutator.symm.trans_le (map_subtype_le _)
+
 instance commutator_characteristic : (commutator G).Characteristic :=
   Subgroup.commutator_characteristic ⊤ ⊤
 

Mathlib/GroupTheory/Solvable.lean

@@ -54,6 +54,14 @@ theorem derivedSeries_normal (n : ℕ) : (derivedSeries G n).Normal := by
 theorem derivedSeries_one : derivedSeries G 1 = commutator G :=
   rfl
 
+theorem derivedSeries_antitone : Antitone (derivedSeries G) :=
+  antitone_nat_of_succ_le fun n => (derivedSeries G n).commutator_le_self
+
+instance derivedSeries_characteristic (n : ℕ) : (derivedSeries G n).Characteristic := by
+  induction n with
+  | zero => exact Subgroup.topCharacteristic
+  | succ n _ => exact Subgroup.commutator_characteristic _ _
+
 end derivedSeries
 
 section CommutatorMap