index_eq_zero_of_relIndex_eq_zero

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If the relative index H.relIndex K equals 0, then H.index equals 0.

Русский

Если H.relIndex K = 0, то H.index = 0.

LaTeX

$$$H.\relIndex K = 0 \Rightarrow H.index = 0$$$

Lean4

@[to_additive]
theorem index_eq_zero_of_relIndex_eq_zero (h : H.relIndex K = 0) : H.index = 0 :=
  H.relIndex_top_right.symm.trans (relIndex_eq_zero_of_le_right le_top h)

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

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

Разделы

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

Аффилиация

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