solvable_of_solvable_injective — Mathlib

English

If f: G →* G' is injective and G' is solvable, then G is solvable (alternative presentation).

Русский

Если инъективен гомоморфизм f: G →* G' и G' разрешим, то G разрешим (вариант формулировки).

LaTeX

$$IsSolvable G$$

Lean4

theorem solvable_of_solvable_injective (hf : Function.Injective f) [IsSolvable G'] : IsSolvable G :=
  solvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot_iff.mpr hf).symm ▸ bot_le)

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