card_mul_index

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If H ≤ G, then |H| · [G:H] = |G| (finite case).

Русский

Если H ≤ G и группа конечна, то мощность H умножить на индекс [G:H] равна мощности G.

LaTeX

$$$ |H| \cdot [G:H] = |G|. $$$

Lean4

@[to_additive (attr := simp) card_mul_index]
theorem card_mul_index : Nat.card H * H.index = Nat.card G :=
  by
  rw [← relIndex_bot_left, ← index_bot]
  exact relIndex_mul_index bot_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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