card_dvd_index

Mathlib.GroupTheory.Sylow

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

← MathLib Explorer

English

The cardinality of Sylow_p(G) divides the index of P in G: |Sylow_p(G)| ∣ index_G(P).

Русский

Число Sylow_p(G) делится на индекс P в G: |Sylow_p(G)| делится на [G : P].

LaTeX

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

Lean4

theorem card_dvd_index [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) : Nat.card (Sylow p G) ∣ P.index :=
  ((congr_arg _ P.card_eq_index_normalizer).mp dvd_rfl).trans (index_dvd_of_le le_normalizer)

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

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

Разделы

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

Аффилиация

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