one_lt_index_of_ne_top

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If H is a proper subgroup of G and G/H is finite, then 1 < H.index.

Русский

Если H является proper-подгруппой G и G/H конечна, то 1 < H.index.

LaTeX

$$1 < H.index$$

Lean4

@[to_additive one_lt_index_of_ne_top]
theorem one_lt_index_of_ne_top [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index :=
  Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨index_ne_zero_of_finite, mt index_eq_one.mp hH⟩

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

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

Разделы

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

Аффилиация

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