derivedSeries_le_map_derivedSeries

English

If f is surjective, then the n-th derived subgroup of G' is contained in the image of the n-th derived subgroup of G: derivedSeries(G',n) ≤ (derivedSeries(G,n)).map f.

Русский

Если f сюръективен, то n-й член производящей серии G' включён в образ n-й члены производящей серии G: derivedSeries(G',n) ≤ (derivedSeries(G,n)).map f.

LaTeX

$$derivedSeries(G',n) ≤ (derivedSeries(G,n)).map f$$

Lean4

theorem derivedSeries_le_map_derivedSeries (hf : Function.Surjective f) (n : ℕ) :
    derivedSeries G' n ≤ (derivedSeries G n).map f := by
  induction n with
  | zero => exact (map_top_of_surjective f hf).ge
  | succ n ih => exact commutator_le_map_commutator ih ih

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