fintypeOfIndexNeZero — Mathlib

English

Let G be a group and H ≤ G with H.index ≠ 0. Then the quotient G/H is finite.

Русский

Пусть G — группа и H является подгруппой G с индексом, отличным от нуля. Тогда фактор-группа G/H конечна.

LaTeX

$$$H.index \neq 0 \Rightarrow \lvert G / H \rvert < \infty$$$

Lean4

/-- Finite index implies finite quotient. -/
@[to_additive /-- Finite index implies finite quotient. -/
    ]
noncomputable def fintypeOfIndexNeZero (hH : H.index ≠ 0) : Fintype (G ⧸ H) :=
  @Fintype.ofFinite _ (Nat.finite_of_card_ne_zero hH)

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