not_dvd_card_ker_transferSylow

Mathlib.GroupTheory.Transfer

URI: https://scilib.ai/kg/mathlib#MonoidHom.not_dvd_card_ker_transferSylow

← MathLib Explorer

English

Under the hypotheses, p does not divide the order of the kernel of the transferSylow map.

Русский

При данных условиях p не делит порядок ядра переноса Sylow.

LaTeX

$$p \nmid |\ker(\operatorname{transferSylow}(P,hP))|$$

Lean4

theorem not_dvd_card_ker_transferSylow : ¬p ∣ Nat.card (transferSylow P hP).ker :=
  (ker_transferSylow_isComplement' P hP).index_eq_card ▸ P.not_dvd_index

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

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

Разделы

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

Аффилиация

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