card_eq_index_normalizer

Mathlib.GroupTheory.Sylow

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

← MathLib Explorer

English

|Sylow_p(G)| = [G : N_G(P)].

Русский

|Sylow_p(G)| = [G : N_G(P)].

LaTeX

$$$|\\mathrm{Sylow}_p(G)| = [G : N_G(P)].$$$

Lean4

theorem card_eq_index_normalizer [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
    Nat.card (Sylow p G) = P.normalizer.index :=
  P.card_eq_card_quotient_normalizer

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

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

Разделы

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

Аффилиация

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