index_eq_one — Mathlib

English

For a subgroup H of G, the index [G:H] equals 1 if and only if H is the whole group G.

Русский

Для подгруппы H в G индекс [G:H] равен 1 тогда и только тогда, когда H = G.

LaTeX

$$$[G:H] = 1 \iff H = G$$$

Lean4

@[to_additive (attr := simp) index_eq_one]
theorem index_eq_one : H.index = 1 ↔ H = ⊤ :=
  ⟨fun h => QuotientGroup.subgroup_eq_top_of_subsingleton H (Nat.card_eq_one_iff_unique.mp h).1, fun h =>
    (congr_arg index h).trans index_top⟩

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