coe_mapSurjective

Mathlib.GroupTheory.Sylow

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

English

The coercion of mapSurjective coincides with the map f on Sylow p-subgroups under surjectivity assumptions.

Русский

Согласование отображения mapSurjective с отображением f на Sylow p-подгруппах при предпосылке сюръективности.

LaTeX

$$P.mapSurjective hf = P.map f$$

Lean4

@[simp]
theorem coe_mapSurjective [Fact p.Prime] (P : Sylow p G) : P.mapSurjective hf = P.map f :=
  rfl

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

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

Разделы

Аффилиация

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