index_eq_card

Mathlib.GroupTheory.Index

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

English

Let G be a group and H a subgroup. Then the index of H in G equals the cardinality of the quotient group G/H.

Русский

Пусть G — группа, H — её подгруппа. Тогда индекс H в G равен кардиналу фактор-группы G/H.

LaTeX

$$$[G:H] = |G/H|$$$

Lean4

@[to_additive]
theorem index_eq_card : H.index = Nat.card (G ⧸ H) :=
  rfl

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

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

Разделы

Аффилиация

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