index_eq_zero_iff_infinite

Mathlib.GroupTheory.Index

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

English

For a subgroup H ≤ G, G/H is infinite if and only if H.index = 0.

Русский

Для подгруппы H ≤ G произведение G/H бесконечно тогда и только тогда, когда H.index = 0.

LaTeX

$$$H.index = 0 \iff Infinite(G / H)$$$

Lean4

@[to_additive]
theorem index_eq_zero_iff_infinite : H.index = 0 ↔ Infinite (G ⧸ H) := by simp [index_eq_card, Nat.card_eq_zero]

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

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

Разделы

Аффилиация

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