index_ne_zero_of_finite

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If the quotient G/H is finite, then H.index ≠ 0.

Русский

Если фактор-группа G/H конечна, то индекс H в G не равен нулю.

LaTeX

$$[G:H] \neq 0 \text{ when } |G/H| < \infty$$

Lean4

@[to_additive]
theorem index_ne_zero_of_finite [hH : Finite (G ⧸ H)] : H.index ≠ 0 :=
  by
  cases nonempty_fintype (G ⧸ H)
  rw [index_eq_card]
  exact Nat.card_pos.ne'

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

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

Разделы

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

Аффилиация

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