finiteIndex_normalCore

Mathlib.GroupTheory.Index

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

English

If H has finite index in G, then its normal core has finite index in G.

Русский

Если H имеет конечный индекс в G, то его нормальное ядро имеет конечный индекс в G.

LaTeX

$$H.normalCore.FiniteIndex$$

Lean4

instance finiteIndex_normalCore [H.FiniteIndex] : H.normalCore.FiniteIndex :=
  by
  rw [normalCore_eq_ker]
  infer_instance

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

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

Разделы

Аффилиация

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