change name

Author: CoolRmal

Mathlib/GroupTheory/Nilpotent.lean

@@ -116,7 +116,7 @@ theorem upperCentralSeriesStep_eq_comap_center :
     div_eq_mul_inv, mul_inv_rev, mul_assoc]
 
 instance [hH : H.Characteristic] : Characteristic (upperCentralSeriesStep H) :=
-  (upperCentralSeriesStep_eq_comap_center H) ▸ comap_Characteristic H centerCharacteristic
+  (upperCentralSeriesStep_eq_comap_center H) ▸ centerCharacteristic.comap_quotient_mk
 
 variable (G)
 

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -392,8 +392,8 @@ theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G
 
 open Subgroup in
 @[to_additive]
-theorem comap_Characteristic [hN : N.Characteristic] {K : Subgroup (G ⧸ N)}
-    (hK : K.Characteristic) :
+theorem _root_.Subgroup.Characteristic.comap_quotient_mk {N : Subgroup G} [hN : N.Characteristic]
+    {K : Subgroup (G ⧸ N)} (hK : K.Characteristic) :
     Characteristic (K.comap (mk' N)) := by
   refine characteristic_iff_map_le.2 fun ϕ x ⟨y, hy⟩ => ?_
   have := characteristic_iff_map_eq.1 hK (congr N N ϕ (characteristic_iff_map_eq.1 hN ϕ))