stabilizer_eq_normalizer

Mathlib.GroupTheory.Sylow

URI: https://scilib.ai/kg/mathlib#Sylow.stabilizer_eq_normalizer

English

The stabilizer of P under the G-action equals the normalizer N_G(P).

Русский

Стабилизатор P при действии G равен нормализатору N_G(P).

LaTeX

$$$\\operatorname{stabilizer}_G(P) = N_G(P).$$$

Lean4

theorem stabilizer_eq_normalizer (P : Sylow p G) : stabilizer G P = P.normalizer := by ext;
  simp [smul_eq_iff_mem_normalizer]

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

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

Разделы

Аффилиация

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