of_finite_quot_finite_subgroup — Mathlib

English

If G is a group and H ≤ G is a finite subgroup with a finite quotient G/H, then G is finite.

Русский

Если G—группа, H ≤ G конечная подгруппа и G/H конечна, то G конечна.

LaTeX

$$$\\text{Finite } H \\land \\text{Finite } (G/H) \\Rightarrow \\text{Finite } G$$$

Lean4

@[to_additive]
theorem _root_.Finite.of_finite_quot_finite_subgroup {H : Subgroup G} [Finite H] [Finite (G ⧸ H)] : Finite G :=
  Finite.of_equiv _ (groupEquivQuotientProdSubgroup (s := H)).symm

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