to_subgroup

Mathlib.GroupTheory.PGroup

URI: https://scilib.ai/kg/mathlib#IsPGroup.to_subgroup

English

If G is a p-group, then every subgroup H ≤ G is also a p-group.

Русский

Если G — p-группа, то любая подгруппа H ≤ G тоже p-группа.

LaTeX

$$IsPGroup p G ⇒ IsPGroup p H for any Subgroup H ≤ G$$

Lean4

theorem to_subgroup (H : Subgroup G) : IsPGroup p H :=
  hG.of_injective H.subtype Subtype.coe_injective

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

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

Разделы

Аффилиация

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