index_toSubgroup

Mathlib.GroupTheory.Index

URI: https://scilib.ai/kg/mathlib#AddSubgroup.index_toSubgroup

← MathLib Explorer

English

The index of the subgroup obtained from H equals H.index: (Subgroup.toSubgroup H).index = H.index.

Русский

Индекс подгруппы, полученной из H, равен H.index.

LaTeX

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

Lean4

@[simp]
theorem _root_.AddSubgroup.index_toSubgroup {G : Type*} [AddGroup G] (H : AddSubgroup G) :
    (AddSubgroup.toSubgroup H).index = H.index :=
  rfl

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

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

Разделы

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

Аффилиация

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