relIndex_eq_zero_of_le_left

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem relIndex_eq_zero_of_le_left (hHK : H ≤ K) (hKL : K.relIndex L = 0) : H.relIndex L = 0 :=
  eq_zero_of_zero_dvd (hKL ▸ relIndex_dvd_of_le_left L hHK)

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

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

Разделы

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

Аффилиация

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