instCoeOutSubgroup

Mathlib.GroupTheory.Sylow

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

English

There is a canonical CoeOut from Sylow p G to Subgroup G, giving an embedding of Sylow subgroups into Subgroup G.

Русский

Существует каноническое вложение из Sylow p G в Subgroup G, отображающее подсистемы Сило в подмножество.

LaTeX

$$$ Sylow_p(G) \\hookrightarrow Subgroup(G) $$$

Lean4

instance : CoeOut (Sylow p G) (Subgroup G) :=
  ⟨toSubgroup⟩

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

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

Разделы

Аффилиация

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