relIndex_dvd_index_of_normal

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If H is normal, relIndex(H, K) divides H.index.

Русский

Если H нормальная, relIndex(H, K) делит H.index.

LaTeX

$$$[H.Normal] : H.relIndex K \\mid H.index$$$

Lean4

@[to_additive]
theorem relIndex_dvd_index_of_normal [H.Normal] : H.relIndex K ∣ H.index :=
  relIndex_sup_right K H ▸ relIndex_dvd_index_of_le le_sup_right

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

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

Разделы

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

Аффилиация

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