normal_of_index_eq_one

Mathlib.GroupTheory.IndexNormal

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

← MathLib Explorer

English

A subgroup with index 1 is normal in the ambient group.

Русский

Подгруппа с индексом 1 нормальна в окружающей группе.

LaTeX

$$H.index = 1 → H.Normal$$

Lean4

/-- A subgroup of index 1 is normal (does not require finiteness of G) -/
theorem normal_of_index_eq_one (hH : H.index = 1) : H.Normal :=
  by
  rw [index_eq_one] at hH
  rw [hH]
  infer_instance

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

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

Разделы

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

Аффилиация

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