instFiniteIndexMin

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If H and K are subgroups of G with finite index, then H ∩ K has finite index in G.

Русский

Если H и K — подгруппы G с конечным индексом, то H ∩ K имеет конечный индекс в G.

LaTeX

$$(H ∩ K).FiniteIndex$$

Lean4

@[to_additive]
instance [FiniteIndex H] [FiniteIndex K] : FiniteIndex (H ⊓ K) :=
  ⟨index_inf_ne_zero FiniteIndex.index_ne_zero FiniteIndex.index_ne_zero⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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