finite_right

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.IsComplement.finite_right

English

If the subgroup H has finite index, then any right transversal T is finite.

Русский

Если индекс подгруппы H конечен, то любой правый трансверсал T конечен.

LaTeX

$$$[H : G] < \\infty \\Rightarrow T\\text{ finite}$$$

Lean4

@[to_additive]
theorem finite_right [H.FiniteIndex] (hT : IsComplement H T) : T.Finite :=
  hT.finite_right_iff.2 ‹_›

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

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

Разделы

Аффилиация

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