relIndex_sup_left

Mathlib.GroupTheory.Index

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

English

If K is normal, relIndex(K, H ⊔ K) = relIndex(K, H).

Русский

Если K нормальная, то relIndex(K, H ⊔ K) = relIndex(K, H).

LaTeX

$$$[K.Normal] : K.relIndex (H \\lor K) = K.relIndex H$$$

Lean4

@[to_additive (attr := simp)]
theorem relIndex_sup_left [K.Normal] : K.relIndex (K ⊔ H) = K.relIndex H := by rw [sup_comm, relIndex_sup_right]

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

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

Разделы

Аффилиация

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