rank_le_index_mul_rank — Mathlib

English

The rank of a subgroup H is at most index(H) times rank(G).

Русский

Ранг подгруппы H не превосходит индекс(H) умножить на ранг G.

LaTeX

$$Group.rank H ≤ H.index · Group.rank G$$

Lean4

theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] : Group.rank H ≤ H.index * Group.rank G :=
  by
  haveI := H.fg_of_index_ne_zero
  obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
  obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS
  calc
    Group.rank H ≤ #T := Group.rank_le hT
    _ ≤ H.index * #S := hT₀
    _ = H.index * Group.rank G := congr_arg (H.index * ·) hS₀

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