index_toAddSubgroup

Mathlib.GroupTheory.Index

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

English

The index of AddSubgroup(H) equals the index of H: (AddSubgroup.toSubgroup H).index = H.index.

Русский

Индекс AddSubgroup(H) равен индексу H: (AddSubgroup.toSubgroup H).index = H.index.

LaTeX

$$(AddSubgroup.toSubgroup H).index = H.index$$

Lean4

@[simp]
theorem index_toAddSubgroup : (Subgroup.toAddSubgroup H).index = H.index :=
  rfl

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

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

Разделы

Аффилиация

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