relIndex_eq_one

Mathlib.GroupTheory.Index

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

English

The relative index H in K is 1 iff K ≤ H.

Русский

Относительный индекс H в K равен 1 тогда, когда K ⊆ H.

LaTeX

$$$H.relIndex K = 1 \iff K \le H$$$

Lean4

@[to_additive (attr := simp) relIndex_eq_one]
theorem relIndex_eq_one : H.relIndex K = 1 ↔ K ≤ H :=
  index_eq_one.trans subgroupOf_eq_top

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

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

Разделы

Аффилиация

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