instFiniteQuotientSubgroupNormalizerOfFactPrime

Mathlib.GroupTheory.Sylow

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

English

If p is prime and Sylow_p(G) is finite, then G / N_G(P) is finite for any P ∈ Sylow_p(G).

Русский

Если p — простое и Sylow_p(G) конечна, то G / N_G(P) конечно для любого P ∈ Sylow_p(G).

LaTeX

$$$|G / N_G(P)| < \\infty.$$$

Lean4

instance [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) : Finite (G ⧸ P.normalizer) :=
  Finite.of_equiv (Sylow p G) P.equivQuotientNormalizer

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

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

Разделы

Аффилиация

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