not_finiteIndex_iff

Mathlib.GroupTheory.Index

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

English

Not H.FiniteIndex if and only if H.index = 0.

Русский

Не FiniteIndex эквивалентно H.index = 0.

LaTeX

$$Not H.FiniteIndex \iff H.index = 0$$

Lean4

@[to_additive]
theorem not_finiteIndex_iff {G : Type*} [Group G] {H : Subgroup G} : ¬H.FiniteIndex ↔ H.index = 0 := by
  simp [finiteIndex_iff]

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

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

Разделы

Аффилиация

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