finiteIndex_iff

Mathlib.GroupTheory.Index

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

English

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

Русский

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

LaTeX

$$Finite(HasQuotient.Quotient G H) \Rightarrow H.FiniteIndex$$

Lean4

@[to_additive]
theorem finiteIndex_iff : H.FiniteIndex ↔ H.index ≠ 0 :=
  ⟨fun h ↦ h.index_ne_zero, fun h ↦ ⟨h⟩⟩

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

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

Разделы

Аффилиация

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