relIndex_eq_zero_of_le_right

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If K ≤ L and H.relIndex K = 0, then H.relIndex L = 0.

Русский

Если K ⊆ L и H.relIndex K = 0, то H.relIndex L = 0.

LaTeX

$$$(hKL : K \le L) \rightarrow (hHK : H.\relIndex K = 0) \rightarrow H.\relIndex L = 0$$$

Lean4

@[to_additive]
theorem relIndex_eq_zero_of_le_right (hKL : K ≤ L) (hHK : H.relIndex K = 0) : H.relIndex L = 0 :=
  Finite.card_eq_zero_of_embedding (quotientSubgroupOfEmbeddingOfLE H hKL) hHK

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

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

Разделы

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

Аффилиация

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