le_normalizer

Mathlib.Algebra.Group.Subgroup.Defs

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

English

Every subgroup is contained in its normalizer: H ≤ N_G(H).

Русский

Каждая подгруппа содержится в своем нормализаторе: H ≤ N_G(H).

LaTeX

$$$H \\le N_G(H)$$$

Lean4

@[to_additive]
theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
  rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]

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

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

Разделы

Аффилиация

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