Each term of the upper central series is characteristic

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

import Mathlib

theorem characteristic_upperCentralSeries (G : Type*) [Group G] (n : ℕ) : (upperCentralSeries G n).Characteristic := by
  sorry

It seems that we don't have this after glancing through Mathlib.GroupTheory.Nilpotent.

[Violeta Hernández]

(should be called characteristic_upperCentralSeries)

[Yongxi Lin (Aaron)]

#34890