finite_quotient_of_finiteIndex

Mathlib.GroupTheory.Index

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

English

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

Русский

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

LaTeX

$$Finite(HasQuotient.Quotient G H)$$

Lean4

@[to_additive]
instance finite_quotient_of_finiteIndex [FiniteIndex H] : Finite (G ⧸ H) :=
  fintypeQuotientOfFiniteIndex.finite

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

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

Разделы

Аффилиация

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