relIndex_dvd_index_of_le

Mathlib.GroupTheory.Index

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

English

If H ≤ K, then H.relIndex K divides H.index.

Русский

Если H ≤ K, то H.relIndex K делит H.index.

LaTeX

$$$H.\\text{relIndex} K \\mid H.\\text{index}$ при $H \\le K$.$$

Lean4

@[to_additive]
theorem relIndex_dvd_index_of_le (h : H ≤ K) : H.relIndex K ∣ H.index :=
  dvd_of_mul_right_eq K.index (relIndex_mul_index h)

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

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

Разделы

Аффилиация

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