card_eq_iff_eq_top — Mathlib

English

The top subgroup has the same cardinality as the ambient group.

Русский

Верхняя подгруппа имеет такую же кардинальность, как сама группа.

LaTeX

$$$\operatorname{Nat}.card(\top : \Subgroup G) = \operatorname{Nat}.card(G)$$$

Lean4

@[to_additive (attr := simp)]
theorem card_eq_iff_eq_top [Finite H] : Nat.card H = Nat.card G ↔ H = ⊤ :=
  Iff.intro (eq_top_of_card_eq H) (fun h ↦ by simpa only [h] using card_top)

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