map_derivedSeries_le_derivedSeries

English

For each n, the image of the n-th derived subgroup under a group hom f satisfies f(derivedSeries(G,n)) ≤ derivedSeries(G',n).

Русский

Образ n-го члена производящей серии под гомоморфизмом f удовлетворяет f(derivedSeries(G,n)) ≤ derivedSeries(G',n).

LaTeX

$$(\\mathrm{derivedSeries}(G,n)).map f \\le \\mathrm{derivedSeries}(G',n)$$

Lean4

theorem map_derivedSeries_le_derivedSeries (n : ℕ) : (derivedSeries G n).map f ≤ derivedSeries G' n := by
  induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Похожие утверждения