to_inf_left

Mathlib.GroupTheory.PGroup

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

English

If H is p-group, then H ∩ K is a p-group.

Русский

Если H — p-группа, то H ∩ K — p-группа.

LaTeX

$$$\IsPGroup(p,H) \rightarrow IsPGroup(p,(H \cap K : Subgroup G))$$$

Lean4

theorem to_inf_left {H K : Subgroup G} (hH : IsPGroup p H) : IsPGroup p (H ⊓ K : Subgroup G) :=
  hH.to_le inf_le_left

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

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

Разделы

Аффилиация

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