exists_comap_subtype_eq

Mathlib.GroupTheory.Sylow

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

← MathLib Explorer

English

There exists Q : Sylow p G such that Q.comap H.subtype = P for P : Sylow p H.

Русский

Существует Q : Sylow p G такой, что Q.comap H.subtype = P для P : Sylow p H.

LaTeX

$$$\\exists Q : Sylow p G, Q.comap H.subtype = P$$$

Lean4

theorem exists_comap_subtype_eq {H : Subgroup G} (P : Sylow p H) : ∃ Q : Sylow p G, Q.comap H.subtype = P :=
  P.exists_comap_eq_of_injective Subtype.coe_injective

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

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

Разделы

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

Аффилиация

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