card_top

Mathlib.Algebra.Group.Subgroup.Finite

URI: https://scilib.ai/kg/mathlib#Subgroup.card_top

English

The cardinality of the top subgroup ⊤ is the same as the cardinality of G.

Русский

Кардинал вершины ⊤ равен кардиналу группы G.

LaTeX

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

Lean4

@[to_additive]
theorem card_top : Nat.card (⊤ : Subgroup G) = Nat.card G :=
  Nat.card_congr Subgroup.topEquiv.toEquiv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru