finite_iff_finite_and_finiteIndex

English

Let G be a group and H a subgroup. Then G is finite if and only if H is finite and the index [G : H] is finite.

Русский

Пусть G — группа, H — подгруппа. Тогда G конечно по мощности тогда и только тогда, когда H конечно и индекс [G : H] конечно.

LaTeX

$$$|G| < \infty \;\Longrightarrow\; (|H| < \infty \;\land\; [G:H] < \infty) \\ (|H| < \infty \land [G:H] < \infty) \Rightarrow |G| < \infty$$$

Lean4

@[to_additive]
theorem finite_iff_finite_and_finiteIndex : Finite G ↔ Finite H ∧ H.FiniteIndex
    where
  mp _ := ⟨inferInstance, inferInstance⟩
  mpr := fun ⟨_, _⟩ ↦
    Nat.finite_of_card_ne_zero <| H.card_mul_index ▸ mul_ne_zero Nat.card_pos.ne' FiniteIndex.index_ne_zero

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